Skip to content

Commit 18a49fc

Browse files
committed
Update HISTORY
1 parent bffd7dd commit 18a49fc

File tree

1 file changed

+15
-0
lines changed

1 file changed

+15
-0
lines changed

HISTORY

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,18 @@
1+
Version 3.0 - 2022-07
2+
3+
LAbS: Added blocks of actions "{a1; a2; ... ; an}"
4+
LAbS: Added block-local variables "var := expr"
5+
LAbS: Added a new rounding integer division operator "e1 : e2"
6+
LAbS: Added lookup operator "var of expr"
7+
LAbS: Added assignment to evaluation of quantified predicates (e.g, "b := forall ..." or "b := exists ...")
8+
LAbS: Added nondeterministic agent selection "pick"
9+
LAbS: Added ternary operator "if cond then expr1 else expr2"
10+
LAbS: Underscores ("_") can now be used within all names (but not at the beginning of a name)
11+
LAbS: Arithmetic expressions can now be used where a Boolean expression is expected ("expr" is desugared into "expr != 0")
12+
13+
SLiVER: CBMC backend now supports simulation
14+
SLiVER: Added a compositional CADP backend "cadp-comp" (experimental)
15+
116
Version 2.1 - 2021-11
217

318
C translation: Fixed a bug with the nondeterministic value operator

0 commit comments

Comments
 (0)