CHANGES 20.1 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.

4
5
6
7
arc 1.5.2:
  Bug fixed:
    . fix missing distribution of altarica-studio

Point Gerald's avatar
Point Gerald committed
8
9
10
11
arc 1.5.1:
  Bug fixed:
    . in bitblaster module, fix ITE bug on integer operands.
  
Point Gerald's avatar
Point Gerald committed
12
13
arc 1.5:
  New features:
Point Gerald's avatar
Point Gerald committed
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
41
42
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
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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
    . 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.
130
131
132
133
arc 1.4.3:
  Bugs fixed:
    . fix memory leak in symbolic to_dot

134
135
136
137
arc 1.4.2:
  Bugs fixed:
    . fix missing domain constraint for enums in FD analysis

Point Gerald's avatar
Point Gerald committed
138
139
140
141
142
arc 1.4.1:
  Bugs fixed:
    . ignore independencies between transitions in reachability algorithm
      for generation of cuts.

point's avatar
point committed
143
144
arc 1.4:
  New features:
145
146
147
    . 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
148
149
150
151
    . 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.
152
153
154
    . implement the function that displays info related to nodes. Displayed info
      are dimensions (i.e. # of vars, # of events, ...) and the underlying 
      hierarchy.
155
    . add support of Mec 5 commands. Commands are not (yet!) interpreted.
Point Gerald's avatar
Point Gerald committed
156
    . #16: clash between identifiers of global enums and subnode.
Point Gerald's avatar
update    
Point Gerald committed
157
    . add new test suite for syntax and static semantics.
Point Gerald's avatar
Point Gerald committed
158
159
160
161
162
163
164
165
166
167
168
169
170
171
    . 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
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
197
198
199
200
201
202
    . 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
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
    . 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
229

Point Gerald's avatar
Point Gerald committed
230
231
232
233
  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
234
    . check that array indexes are computable constants.
Point Gerald's avatar
Point Gerald committed
235
236
237
238
239
    . 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
240
241
242
    . 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
243
244
245
246
247
248
249
250
251
252
253
    . 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
254

255
256
257
258
arc 1.3.5 :
 Bug fixes:
    . update install-arc.sh

Point Gerald's avatar
Point Gerald committed
259
260
261
262
263
264
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
265
266
267
268
269
270
271
272
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
273
274
275
276
277
278
279
280
281
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
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
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.

319
arc 1.2:
point's avatar
update    
point committed
320
 New features:
point's avatar
point committed
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
    . 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
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
    . 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).
389
390
391
    . install documentation into standard location
    . add a short README, NEWS and CHANGES files 
    . add pkg-config support
point's avatar
update    
point committed
392
393
394
395
396
    . 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
397
398
 Bug fixing:
    . in quot, the transitions was not simplified. remove redundant ones. 
point's avatar
update    
point committed
399
    . error in the project algorithm used by acheck 
point's avatar
point committed
400
    . remove several memory leaks