CHANGES 8.35 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
arc 1.4:
  New features:
6
7
8
    . add a by-extension preprocessing mechanism. A preprocessor can be 
      associated to a filename extension. A default preprocessor can also be
      defined.
Point Gerald's avatar
Point Gerald committed
9
10
11
12
    . 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.
13
14
15
    . implement the function that displays info related to nodes. Displayed info
      are dimensions (i.e. # of vars, # of events, ...) and the underlying 
      hierarchy.
16
    . add support of Mec 5 commands. Commands are not (yet!) interpreted.
Point Gerald's avatar
Point Gerald committed
17
    . #16: clash between identifiers of global enums and subnode.
Point Gerald's avatar
update    
Point Gerald committed
18
    . add new test suite for syntax and static semantics.
point's avatar
point committed
19

Point Gerald's avatar
Point Gerald committed
20
21
22
23
  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.
Point Gerald's avatar
update    
Point Gerald committed
24
    . check that array indexes are computable constants.
Point Gerald's avatar
Point Gerald committed
25

Point Gerald's avatar
Point Gerald committed
26
27
28
29
30
31
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.

Point Gerald's avatar
Point Gerald committed
32
33
34
35
36
37
38
39
arc 1.3.3 :
 Bug fixes:
    . fix bug in symbolic "quot"

arc 1.3.2 :
 Bug fixes:
    . fix a bug related to parameter instanciation

point's avatar
point committed
40
41
42
43
44
45
46
47
48
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.

point's avatar
point committed
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
84
85
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.

86
arc 1.2:
point's avatar
update    
point committed
87
 New features:
point's avatar
point committed
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
    . 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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
    . 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).
156
157
158
    . install documentation into standard location
    . add a short README, NEWS and CHANGES files 
    . add pkg-config support
point's avatar
update    
point committed
159
160
161
162
163
    . 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
164
165
 Bug fixing:
    . in quot, the transitions was not simplified. remove redundant ones. 
point's avatar
update    
point committed
166
    . error in the project algorithm used by acheck 
point's avatar
point committed
167
    . remove several memory leaks