Commit 58121def authored by Point Gerald's avatar Point Gerald
Browse files

- add missing chkctl page

- update CHANGES for 1.5
parent fe1d3b2b
......@@ -3,8 +3,122 @@ Details can be found in the ChangeLog file.
arc 1.5:
New features:
Bug fixed:
. add dot-func-deps option that permits to display functional dependencies
in DOT format.
. disable display of epsilon events in broadcast vectors.
. add last-chance garbage collection when memory is exhausted.
. remove creation of _idle variable when parse tree is interpreted.
. add branch of the repository to version data.
. add several lazy operations for manipulation of relations.
. add altarica-studio-simulator
. add 'validate' command for Acheck specs.
. enforce lexicographical order to display broadcast vectors.
. subnodes array are not split by projection.
. add 'empty_s' and 'empty_t' predefined properties
. allow the AltaRica parser to accept CTL* spec separately.
. Acheck 'eval' command now support EOF tag like '<<' redirection for shell
programs.
. add new command 'chkctl' that checks if initial configurations of a node
satisfy a given CTL property and display, according to the result, a
witness or a counterexample.
. load preferences according to ARC_DATADIR environment variable.
. add a new dialog box to Studio Simulation that permits to select
variables displayed in the tree displaying configurations.
. check ARC_DATADIR environment variable to determine the location
of online documentation.
. separate cuts and sequences computation into two different commands
. add option --enum used to specify if ARC enumerates cuts/sequences or
output them as a Boolean formula.
. environment variable ARCPATH is now used to look for files loaded with
'load' command.
. disable object replacement. Now an error is generated when one try to
redefine an element of the model.
. add 'all' argument to 'remove' command.
. add computation for universally quantified guards on 'project' command.
. add 'dot'-trace command that outputs a trace in dot format.
. add a Graph tab to Studio that allows to display dot graphs generated by
Acheck specs (dot, quot and dot-trace).
. remove default preprocessor that can be not present on the system where
ARC is installed.
. change dot output for states. Four modes are now available to display
states: none, post, pre, both. The mode is set using preferences called
acheck.dot-diff-state-mode. According to the selected mode, 'dot' command
displays a state using only variables that differ with the specified
neighborhood.
. add option to command 'validate' that enable/disable computation of
reachables.
. change FD computation to favor equations of the form f = F(s,f') where
F is not a simple flow variable.
. add prefix parameter to commands 'cuts' and 'sequences'
. add --help option
. lazy loading of man pages to prevent warnings before the binding of
listeners.
. rename max-card into max-conf-card in node-info sub-commands
. remove altarica to fast translator.
. add 'pages' help page.
. add subcommand to 'info' that gives ordering of relations variables
. add 'cd' and 'pwd' commands
. testsuite now refers to ARC in builddir and not the one currently
installed.
. Files opened in acheck context are now search into ARCPATH variable.
. add 'dd' subcommand to 'info' to display dot graph of the DD encoding a
relation.
. add 'sat' and diag' experimental commands
. for preprocessing, replace the use of 'popen' function by the creation of
a temporary file
. add non-regression test-suite for computation of cuts.
. add 'modes' command to acheck that produce a dot file
containing mode-automaton of the specified node. Vertices of the graph
are control states of the node. Edges are labelled with a formula that
describes values of flows allowing the state change and the event of the
associated transition.
. add new bang-id 'nsemove' that gives moves without epsilon self-loops.
. add generation of a DOT file for counter examples.
. add 'dd-all-paths' and 'dd-assignments' that displays in dot format a DD
with all paths or restricted to accepting paths.
. integrate Glucose SAT solver.
. use Glucose to check satisfiability of boolean expr when it is possible.
. add 'root-nodes' sub-command to 'info'
. add computation of constant state variables in the computation of
functional dependencies.
. permit 'solve' command to call the solver on a given expression.
. allow backslashed characters in shell quoted-strings.
. add a prefix to gates of generated Aralia formulas.
. add options to 'depgraph' command to display events or not.
. add test-suite for diag command
. remove libaltarica and move parser into src directory.
. change behavior of 'validate --reach'; see help validate.
. add '--algo=' option to 'obfuscate' command.
. add mec5-builtins, acheck-commands and acheck-builtins help pages.
. add 'quit' as an alias for 'exit'
Bugs fixed:
. minor bug in func-deps display
. fix several memory leaks
. fix a minor bug in computation of DD statistics
. in ordering of variables, fix initialization of list variables for
a transition.
. fix bug in output of array of subnodes fields.
. fix output of expressions for project operator.
. 'false' assertion produced a non-empty model. Assertion was ignored by
the procedure that computes assertions.
. fix !move relation
. fix quot bug for empty systems.
. fix handling of syntax errors in acceptance formula of cuts.
. in sequence generate, fix case where only one event is observed generated
a bug due to EXHAUSTIVE encoding of sequences.
. fix maximal number of references to a DD.
. fix bug in bitblasting of ite.
. GC now actually free nodes.
. fix test-cases that did not load correct files.
. fix missing use of invariants in postpre.
. in FD computation, fix case where no assertion exists.
. fix handbook generated pages
. fix generation of rewritten ca
. fix newly introduced 't' attribute. Not supported by xdot.
. fix exhaustive stepper bug. sparse sets of enum where mismanaged.
. fix a memory leak in pick_one_element
. fix toolbar icons of AS simulator.
arc 1.4.3:
Bugs fixed:
. fix memory leak in symbolic to_dot
......
......@@ -14,6 +14,7 @@ CMDLINE_HELP_FILES = \
card-cmd.texi \
cd-cmd.texi \
check-card-cmd.texi \
chkctl-cmd.texi \
cuts-cmd.texi \
depgraph-cmd.texi \
diag-cmd.texi \
......
......@@ -183,6 +183,9 @@ should display the list of user preferences using the pager command
@subsection @command{validate}
@include validate-cmd.texi
@subsection @command{chkctl}
@include chkctl-cmd.texi
@section Commands related to computations using exhaustive engine
@subsection @command{ts}
......
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