Commit 0e46bf34 authored by Point Gerald's avatar Point Gerald
Browse files

register changes

parent 2947b6bb
......@@ -61,6 +61,32 @@ arc 1.4:
stream is indicated either by an end-of-file character (e.g ^D) or by an
explicit keyword given as parameter (default=EOF).
. allows two modes for the 'eval' command (batch or interactive).
. sets computed with Acheck can be reused in Mec 5 specifications
. add timer command that permits to create timers to evaluate execution
time of ARC commands
. AND assertions are automatically splitted
. store reduced CA into its source CA.
. Compute minimal cutsets. Use wdd to compute them applying A.Rauzy
algorithm.
. check in initial clause if assigned value is in domain of the variable
. change DD index management. Add a new module that store index and
dd-index of variables.
. extend DD api: add ar_dd_cardinality, add ar_dd_pick, add functions to
create lists of variables, ar_dd_project_on_variables with relabelling
. tests now don't use anymore installed ARC but the one compiled
${top_builddir}/src
. integrate CCL into ARC package. The library is automatically downloaded
from GIT repository when bootstrap.sh script is invocated.
. pre-compute hash value of expressions
. ar_dd_project_on_variables in place of several ad hoc functions
. use ar_solver instead of a brut-force computation of constraints in
expr2dd function
. rewrite EQ formula in the case where an operand is an ITE formula.
. when computing reachable configuration, checks if the model possesses an
'do-nothin' macro-transition (normally it should have one). In this case
S \subseteq post(S).
. 'symbolically' keyword is now the default for acheck specifications.
'exhaustively' must be used to use explicit graph.
Bug fixed:
. #15: clash between identifiers of events and global enums. An enumeration
......@@ -75,7 +101,17 @@ arc 1.4:
. fix error in indexation of quantified variables.
. fix memory leak in computation of reachables. global assertion wasn't
unreferenced.
. minor fix in shell grammar.
. composite variables were not correctly flatten.
. in enumeration of paths when displaying the DD solutions. For DD=one
nothing was displayed.
. #31: array containing post_conditions was not computed prior the
computation of pre-defined sets.
. #32: bounds of enum domain were used in place of cardinality.
. #33: since lazy evaluation of assertions an error has been introduced in
valid_state_assignments computation. Projection on state variables was
made only on the 1st assertion.
. fix stack overflow in shell parser.
arc 1.3.5 :
Bug fixes:
......
......@@ -7,8 +7,8 @@ What's new in 1.4:
* the 'info' command now displays dimension of nodes and their hierachy
* Mec 5 commands in specs files don't yield syntax error.
* make DD variables ordering less dependant of the syntax
* add generation of cuts. Result is a Boolean formula that can be treated with
Aralia. Visible events can be distinguished from others.
* add generation of (minimal) cuts. Visible events can be distinguished from
others. Tags can be used to disable useless events.
* 'list nodes' now adds a star to root nodes
* changes to 'eval' command:
. adds a new preference that permits to set the prompt displayed by the
......@@ -24,20 +24,33 @@ What's new in 1.4:
. target-reduction: project a node on the sub-part that influences the value
of a given formula.
. depgraph: gives info related to dependencies in a CA
. node-info: returns infos about a node (childs, max-card, variables, ...)
. stepper command used as a textual step-by-step simulator
. node-info: returns infos about a node (children, max-card, variables, ...)
. stepper: used as a textual step-by-step simulator
. timer: permits to create timers to evaluate execution time of ARC commands
. cuts: permit to compute (minimal) sequences that yield a failure
* new options:
. -x : enable command/response mode that disables readline interactions
and remove decoration of outputs. This mode is suitable with interaction
with another process.
. -l logfile: permit to log all outputs of the program to a given file
. -V, --version: display verbose informations about ARC. -q can be used to
get only the release number
* acheck changes:
. add 'assert' operator to specifications that restricts a set of states to
valid configurations
. add 'events' command to Acheck specifications that displays events
labelling a set of transitions
. sets computed with Acheck can be reused in Mec 5 specifications
* add Altarica Studio GUI for ARC
* CCL and ARsyntax integration into ARC:
. CCL is now present in ARC distribution file and installed automatically. IF
GIT is used, CCL is automatically downloaded from repository when
bootstrap.sh script is invocated.
. Altarica parser is integrated into ARC distribution. ARsyntax is not
required anymore.
* Symbolic representation of graph using DDs is now the default with Acheck
specifications. 'exhaustively' keyword must be used to enable explicit graph.
What's new in 1.3:
* add ARC handbook.
* add experimental 'sequences' command that should produces sequences leading
......
Supports Markdown
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