CHANGES 13.8 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 Gerald's avatar
Point Gerald committed
4
5
6
7
arc 1.5:
  New features:
  Bug fixed:

8
9
10
11
arc 1.4.3:
  Bugs fixed:
    . fix memory leak in symbolic to_dot

12
13
14
15
arc 1.4.2:
  Bugs fixed:
    . fix missing domain constraint for enums in FD analysis

Point Gerald's avatar
Point Gerald committed
16
17
18
19
20
arc 1.4.1:
  Bugs fixed:
    . ignore independencies between transitions in reachability algorithm
      for generation of cuts.

point's avatar
point committed
21
22
arc 1.4:
  New features:
23
24
25
    . 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
26
27
28
29
    . 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.
30
31
32
    . implement the function that displays info related to nodes. Displayed info
      are dimensions (i.e. # of vars, # of events, ...) and the underlying 
      hierarchy.
33
    . add support of Mec 5 commands. Commands are not (yet!) interpreted.
Point Gerald's avatar
Point Gerald committed
34
    . #16: clash between identifiers of global enums and subnode.
Point Gerald's avatar
update    
Point Gerald committed
35
    . add new test suite for syntax and static semantics.
Point Gerald's avatar
Point Gerald committed
36
37
38
39
40
41
42
43
44
45
46
47
48
49
    . 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    
Point Gerald's avatar
Point Gerald committed
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
    . 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).
Point Gerald's avatar
Point Gerald committed
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
    . 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.
Point Gerald's avatar
Point Gerald committed
107

Point Gerald's avatar
Point Gerald committed
108
109
110
111
  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
112
    . check that array indexes are computable constants.
Point Gerald's avatar
Point Gerald committed
113
114
115
116
117
    . 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    
Point Gerald's avatar
Point Gerald committed
118
119
120
    . fix error in indexation of quantified variables.
    . fix memory leak in computation of reachables. global assertion wasn't 
      unreferenced.
Point Gerald's avatar
Point Gerald committed
121
122
123
124
125
126
127
128
129
130
131
    . 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.    
Point Gerald's avatar
Point Gerald committed
132

133
134
135
136
arc 1.3.5 :
 Bug fixes:
    . update install-arc.sh

Point Gerald's avatar
Point Gerald committed
137
138
139
140
141
142
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
143
144
145
146
147
148
149
150
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
151
152
153
154
155
156
157
158
159
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
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
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.

197
arc 1.2:
point's avatar
update    
point committed
198
 New features:
point's avatar
point committed
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
    . 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
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
    . 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).
267
268
269
    . install documentation into standard location
    . add a short README, NEWS and CHANGES files 
    . add pkg-config support
point's avatar
update    
point committed
270
271
272
273
274
    . 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
275
276
 Bug fixing:
    . in quot, the transitions was not simplified. remove redundant ones. 
point's avatar
update    
point committed
277
    . error in the project algorithm used by acheck 
point's avatar
point committed
278
    . remove several memory leaks