CHANGES

-*- mode : org; -*-

This file is a brief description of changes in this new release of ARC.
Details can be found in the ChangeLog file.

* arc 1.6
** New features
- add external clauses for the description of stochastic data
- add a Monte-Carlo engine (see handbook for details)
- Mec5 relations defined by the user can contain !. If a relation is over configurations it becomes available in Acheck context.
- add a Boolean in 'test' Acheck command that permits to generate a counter-example/witness.
- AltaRica Studio now checks if ARC environment variable is set to call arc executable.
- clarify public event semantics wrt to parents: does not generate code for public events that are already declared in parent node. 
- enable a direct access to Glucose solver from command line (cf. solver command)
- add display of rusage at exit of arc (cf. arc.shell.rusage preference)
- disallow sync vectors in leaf nodes
    
** Bug fixed/Improvement
- fix lexical analysis of CPP relocation lines
- fix the build of Windows Installer for MSYS2/MINGW
- improve flattening and translation to CA
- improve configuration files 
- extend tests suites (add perf test-suite)
- improve determinism of execution (make data-structure less dependant from pointers).
- limit computation of constant state variables in order to reduce cost.
- add rewriting function wrt to FD but with bound on the size of generated expressions or depth of replacement.
- fix the display of nodes with no explicit event.

* arc 1.5.2
** Bug fixed
- fix missing distribution of altarica-studio

* arc 1.5.1
** Bug fixed
- in bitblaster module, fix ITE bug on integer operands.
  
* arc 1.5
** New features
- 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

* arc 1.4.2
** Bugs fixed
- fix missing domain constraint for enums in FD analysis

* arc 1.4.1
** Bugs fixed
- ignore independencies between transitions in reachability algorithm
for generation of cuts.

* arc 1.4
** New features
- add a by-extension preprocessing mechanism- A preprocessor can be 
      associated to a filename extension- A default preprocessor can also be
      defined.
- add 'attribute id' formula in Acheck specifications that is the set of
      transitions whose event contains a component with the attribute 'id'.
- add CTL* logic into acheck specifications- Formulas are introduced using
      ctlspec keyword.
- implement the function that displays info related to nodes- Displayed info
      are dimensions (i.e- # of vars, # of events, ...) and the underlying 
      hierarchy.
- add support of Mec 5 commands- Commands are not (yet!) interpreted.
- #16: clash between identifiers of global enums and subnode.
- add new test suite for syntax and static semantics.
- add a command/response mode (-x) that disable readline interactions and 
      remove decoration of outputs
- add node-info commands that return infos about a node (childs, max-card,
      variables, ...)
- add a option that permit to log all outputs of the program to a given file
- add Altarica Studio GUI for ARC
- replaces fixed size buffer of readline-no-rl by a dynamically cc-buffer
- extend CA API with iterators to CA fields
- add 'stepper' command used as a textual step-by-step simulator
- add 'assert' operator to Acheck specifications that restricts a set of 
      states to valid configurations
- add 'events' command to Acheck specifications that displays events 
      labelling a set of transitions
- lazy evaluation of the conjunction of assertions    
- add functional dependencies analysis to CAs- 
- add computation of a dependency graph for components (vars, asserts, 
      transitions) of a CA
- add a function to reindex variables of CA
- add functional analysis at the end of the constuction of a CA.
- partitions assertions into constraints and functional dependencies
- add reduction of a CA wrt to a dependency graph
- add 'arch' command that generate a DOT file with the architecture of
      a hierarchical node
- add 'target-reduction' command that project a node on the sub-part that
      influence the value of a given formula.
- factorize code between explicit/symbolic sequence generators
- make DD variables ordering less dependant of the syntax
- propagate attributes of variables into the CA.
- in variable ordering for DDs gather variables assigned by a transition
- change the display of a CA using one variable per line
- in DD module add a projection function- Use a DD to encode list of 
      variables
- compute dependencies between transitions and use it for sequences 
      generation
- add generation of cuts encoded by a Boolean formula.
- add the possibility to indicate a tag that marks visible events used by
      the cut generator- by default all are visible
- in 'list nodes', add a star to root nodes
- add 'depgraph' command that gives info related to dependencies in a CA
- adds a new preference that permits to set the prompt displayed by the
      "eval" command
- 'eval' command now support Readline- The end of the input
      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
      type has been added to each node- This enumeration defines the type of
      events of that node.
- check that array indexes are computable constants.
- fix several wrong or missing error codes in arc commands
- fix a bug related to ARC_SHELL_CURRENT_CONTEXT that can be NULL in 
      non-interactive mode
- change shell parser to return asap in order to prevent stack-overflow in
      yyparse    
- 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
- update install-arc.sh

* arc 1.3.4
** Bug fixes
- issue #30: in ar_ts_display_trans, the same state was used for the source and the tgt of  the transitions- Reference to event was not suppressed before return.

* arc 1.3.3
** Bug fixes
- fix bug in symbolic "quot"

* arc 1.3.2
** Bug fixes
- fix a bug related to parameter instanciation

* arc 1.3.1
** Bug fixes
- fix memory leak in ar_poset_dup
- in seq-cmd.c the constraint automaton was not computed from the flatten semantics but on the node itself.
- memory leak fixed in sequence generator, some states were lost.
- in sequence generator, the callback passed to ccl_graph_dfs returned a bad code that forbid the visit of parts of the dependency graph.

* 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 
- add 'card' command that display the cardinality of a Mec5 relation
- Mec5 relation can be displayed using the 'show' command.
- add "!st" predefined relation
- add the 'eval' command that allows to evaluate an AltaRica node, a MEC 5 or ACHECK spec from the command line
- add a test suite for MEC5 specs
- add 'check-card' command to test cardinality of a set- If the preference arc.shell.check-card-abort = true then ARC is aborted when a test fails.
- the 'set' command now takes two options (-load, -save) used to save or to load preferences into/from the ~/.arcrc file- This mechanism replaces the implicit saving of preferences when ARC terminates.
- add the N!vars type that represents any assignments of variables from the node N- The assignment can satisfy or not the assertions.
- replace N!c by N!vars in the signature of N!st.
- add the N!reach : N!c relation that is a precomputation of the reachable configurations of N.
- split behaviors of the 'show' command in two separate commands, 'list' and 'show'.
- add arc.shell.preprocessor preference
- preprocess AltaRica/Mec5/Acheck file with the specified command.
- add the relation !vs a subset of !sc encoding assignments of state variables that can satisfy assertions.
- add the relation !vsc that encodes transitions between elements of !vs
- add 'gc' command that explicitly call the garbage collector on DDs.
- add 'store' command used to dump Mec 5 relations into a file. File name extension must be '.rel' to be reloaded later- Stored relations are appended to the end of file (i.e- the file is not erased). If the signature of the relation contains bang ids then store associated relations (if non trivial).
- add 'info' command that displays informative infos about given identifiers
- add 'remove' command that releases resources allocated to an ARC object
- add the 'pick' command that creates a new relation from an existing one, say R, by taking one element in R.
- for compatibility with Mec5, add an inactive transition for events without one. Emit a warning if an event is declared but never used in a transition.
- add to the 'ca' command the '-mec' option that should generate AltaRica nodes in  a syntax compliant with Mec 5.
- remove handling of command 'calls' as parameters
- disable SIGINT handler before calls to ARC commands.
- start a non-regression test suite.
- acheck specifications can be computed using Decision Diagrams (DD) of Toupie.
- add several operations to be used within the DD mode of acheck:
  + proj_s (resp- proj_f) that projects a relation on state (resp- flow) 
    variables
  + pick that extracts a singleton from a relation-      
- add several predefined set to be used within the DD mode of acheck:
  + any_trans is the relation produced by transitions alone i.e- without pre and post conditions.
  + any_c is the relation produced by the assertion of the node i.e. the set of all allowed (by not necessarily reachable) configurations
  + valid_state_assignments is the projection of any_c on state variables.
  + valid_state_changes is the projection on state variables of the          transition relation between allowed configurations.
- add the 'run' command that starts a graphical simulator (that replaces the altatools one) based on the GTK+ toolkit.
- constraint automata (produced with the 'ca' command) are now displayed as AltaRica nodes.
- add "-c <cmd>" command-line option that permits to execute an ARC script.
- add "-q" command-line option that disables information messages.
- add the 'set' command that permits to list/view/change ARC preferences.
- add new preferences (entries in ~/.arcrc) for acheck:
  + acheck.timers (default = false) that enables timers on computations of equations.
  + acheck.cleanup-semantics (default = false) that requests arc to clean up computed semantics (with computed properties).
- install documentation into standard location
- add a short README, NEWS and CHANGES files 
- add pkg-config support
- add autoconf/automake support
- add several Lustre translators tests
- implements the linear model-checking algoritm in place of the quadratic one.

** Bug fixing
- in quot, the transitions was not simplified. remove redundant ones.
- error in the project algorithm used by acheck 
- remove several memory leaks