Commit f0fd4ef3 authored by point's avatar point
Browse files

update for 1.3

parent e3d430fc
This file is a brief description of changes in this new release of ARC.
Details can be found in the ChangeLog file.
arc 1.3:
New features:
. add ARC handbook.
. add experimental 'sequences' command that should produces sequences
leading an AltaRica node into unexpected states.
. in Acheck specs, more commands are available with DDs: trace, dot, quot,
project
. explicit representation now encodes values with 'int'.
. add timers for Mec 5 computations. Timers are enabled using "mec5.timers"
setting.
. in the simulator, add a button that generates the current assignment of
state variables as an "init" clause.
. show(all) now order properties lexicographically.
. add the 'validate' command that checks some small properties of nodes
(e.g. domains coverage, macro-transitions usage, ...)
. add an 'obfuscation' command permitting to obfuscate models and specs.
. display a warning message when two enums with no intersection are
compared.
. in Acheck specs, TEST(X) behaves like check-card i.e. checks the
non-emptiness of X
. support additional constraint for the initial configuration.
Bug fixing:
. DD engine did not handle correctly the case where an assertion was simply
"true".
. check that values assigned to "const" symbols are in the given domain.
. DD engine handled incorrectly domains of variables declared equal by
assertions. When domains differed (e.g. two different ranges) one
variable could be assigned the domain of the other.
. cell collector of the backtracking stack of the solver was not used.
. Flow variables could be assigned by transitions
. show-ts-marks treated only its first argument.
. double deallocation in 'pick' command yielding a segfault.
. bug fixed in fixpoint computation for unavoidable configurations ('unav')
in explicti representation.
. visibility was not checked in guards.
arc 1.2:
New features:
. add an interpreter for Mec5 specifications
......
ARC NEWS - History of user visible changes.
Copyright (C) 2007-2009 Alain Griffault, Gerald Point, Aymeric Vincent
What's new in 1.3:
* add ARC handbook.
* add experimental 'sequences' command that should produces sequences leading
an AltaRica node into unexpected states.
* in Acheck specs, more commands are available with DDs: trace, dot, quot,
project.
* explicit representation now encodes values with 'int'.
* add timers for Mec 5 computations. Timers are enabled using "mec5.timers"
setting.
* in the simulator, add a button that generates the current assignment of
state variables as an "init" clause.
* show(all) now order properties lexicographically.
* add the 'validate' command that checks some small properties of nodes
(e.g. domains coverage, macro-transitions usage, ...)
* add an 'obfuscation' command permitting to obfuscate models and specs.
* display a warning message when two enums with no intersection are compared.
* in Acheck specs, TEST(X) behaves like check-card i.e. checks the
non-emptiness of X
* support additional constraint for the initial configuration.
What's new in 1.2:
* Add pkg-config support.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment