CHANGES 6.58 KB
Newer Older
1
2
3
This file is a brief description of changes in this new release of ARC.
Details can be found in the ChangeLog file.

point's avatar
point committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
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.

41
arc 1.2:
point's avatar
update    
point committed
42
 New features:
point's avatar
point committed
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
    . 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.
point's avatar
update    
point committed
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
    . 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).
111
112
113
    . install documentation into standard location
    . add a short README, NEWS and CHANGES files 
    . add pkg-config support
point's avatar
update    
point committed
114
115
116
117
118
    . add autoconf/automake support
    . add several Lustre translators tests
    . implements the linear model-checking algoritm in place of the quadratic
      one.

point's avatar
point committed
119
120
 Bug fixing:
    . in quot, the transitions was not simplified. remove redundant ones. 
point's avatar
update    
point committed
121
122
    . error in the project algorithm used by acheck 
    . remove several memory leaks