CHANGES 20.8 KB
Newer Older
Point Gerald's avatar
Point Gerald committed
1
2
-*- mode : org; -*-

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

6
7
8
* arc 1.6.2
** New features
** Bug fixed/Improvements
9
- fix erroneous deletion of check-mincuts.test in test suite
Point Gerald's avatar
Point Gerald committed
10
- fix renated urls
11

Point Gerald's avatar
Point Gerald committed
12
* arc 1.6.1
13
14
15
** New features
- dot(S,T) now outputs the sub-graph induced by S and not only the part reachable from the initial states.

Point Gerald's avatar
Point Gerald committed
16
** Bug fixed/Improvements
Point Gerald's avatar
Point Gerald committed
17
- fix bug in attributes of 'quot' command
18
- check the size of array expressions when a size of requested
Point Gerald's avatar
update    
Point Gerald committed
19
20
- fix propagation of constants in FD detection for state variables
- add small simplification rules for arithmetic operators in CA expressions
Point Gerald's avatar
Point Gerald committed
21
- fix distribution of altarica-studio sources in absence of pre-requisites
22
23
- fix a circular dependency for the compilation of the handbook

Point Gerald's avatar
Point Gerald committed
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
* 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
50

Point Gerald's avatar
Point Gerald committed
51
52
53
* arc 1.5.1
** Bug fixed
- in bitblaster module, fix ITE bug on integer operands.
Point Gerald's avatar
Point Gerald committed
54
  
Point Gerald's avatar
Point Gerald committed
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
* 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 
Point Gerald's avatar
Point Gerald committed
95
      installed.
Point Gerald's avatar
Point Gerald committed
96
97
- 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
Point Gerald's avatar
Point Gerald committed
98
      relation.
Point Gerald's avatar
Point Gerald committed
99
100
- add 'sat' and diag' experimental commands
- for preprocessing, replace the use of 'popen' function by the creation of
Point Gerald's avatar
Point Gerald committed
101
      a temporary file
Point Gerald's avatar
Point Gerald committed
102
103
104
105
- 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
Point Gerald's avatar
Point Gerald committed
106
107
      describes values of flows allowing the state change and the event of the
      associated transition.
Point Gerald's avatar
Point Gerald committed
108
109
110
- 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 
Point Gerald's avatar
Point Gerald committed
111
      with all paths or restricted to accepting paths.
Point Gerald's avatar
Point Gerald committed
112
113
114
115
- 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
Point Gerald's avatar
Point Gerald committed
116
      functional dependencies.
Point Gerald's avatar
Point Gerald committed
117
118
119
120
121
122
123
124
125
126
- 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'
Point Gerald's avatar
Point Gerald committed
127
    
Point Gerald's avatar
Point Gerald committed
128
129
130
131
132
    ** 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 
Point Gerald's avatar
Point Gerald committed
133
      a transition.
Point Gerald's avatar
Point Gerald committed
134
135
136
- 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 
Point Gerald's avatar
Point Gerald committed
137
       the procedure that computes assertions.
Point Gerald's avatar
Point Gerald committed
138
139
140
141
- 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
Point Gerald's avatar
Point Gerald committed
142
      a bug due to EXHAUSTIVE encoding of sequences.
Point Gerald's avatar
Point Gerald committed
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
- 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
159

Point Gerald's avatar
Point Gerald committed
160
161
162
* arc 1.4.2
** Bugs fixed
- fix missing domain constraint for enums in FD analysis
163

Point Gerald's avatar
Point Gerald committed
164
165
166
167
* arc 1.4.1
** Bugs fixed
- ignore independencies between transitions in reachability algorithm
for generation of cuts.
Point Gerald's avatar
Point Gerald committed
168

Point Gerald's avatar
Point Gerald committed
169
170
171
172
* 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
173
      defined.
Point Gerald's avatar
Point Gerald committed
174
- add 'attribute id' formula in Acheck specifications that is the set of
Point Gerald's avatar
Point Gerald committed
175
      transitions whose event contains a component with the attribute 'id'.
Point Gerald's avatar
Point Gerald committed
176
- add CTL* logic into acheck specifications- Formulas are introduced using
Point Gerald's avatar
Point Gerald committed
177
      ctlspec keyword.
Point Gerald's avatar
Point Gerald committed
178
179
- implement the function that displays info related to nodes- Displayed info
      are dimensions (i.e- # of vars, # of events, ...) and the underlying 
180
      hierarchy.
Point Gerald's avatar
Point Gerald committed
181
182
183
184
- 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 
Point Gerald's avatar
Point Gerald committed
185
      remove decoration of outputs
Point Gerald's avatar
Point Gerald committed
186
- add node-info commands that return infos about a node (childs, max-card,
Point Gerald's avatar
Point Gerald committed
187
      variables, ...)
Point Gerald's avatar
Point Gerald committed
188
189
190
191
192
193
- 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 
Point Gerald's avatar
Point Gerald committed
194
      states to valid configurations
Point Gerald's avatar
Point Gerald committed
195
- add 'events' command to Acheck specifications that displays events 
Point Gerald's avatar
Point Gerald committed
196
      labelling a set of transitions
Point Gerald's avatar
Point Gerald committed
197
198
199
- lazy evaluation of the conjunction of assertions    
- add functional dependencies analysis to CAs- 
- add computation of a dependency graph for components (vars, asserts, 
Point Gerald's avatar
Point Gerald committed
200
      transitions) of a CA
Point Gerald's avatar
Point Gerald committed
201
202
203
204
205
- 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
Point Gerald's avatar
Point Gerald committed
206
      a hierarchical node
Point Gerald's avatar
Point Gerald committed
207
- add 'target-reduction' command that project a node on the sub-part that
Point Gerald's avatar
Point Gerald committed
208
      influence the value of a given formula.
Point Gerald's avatar
Point Gerald committed
209
210
211
212
213
214
- 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 
Point Gerald's avatar
Point Gerald committed
215
      variables
Point Gerald's avatar
Point Gerald committed
216
- compute dependencies between transitions and use it for sequences 
Point Gerald's avatar
Point Gerald committed
217
      generation
Point Gerald's avatar
Point Gerald committed
218
219
220
221
222
223
- 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
Point Gerald's avatar
Point Gerald committed
224
      "eval" command
Point Gerald's avatar
Point Gerald committed
225
- 'eval' command now support Readline- The end of the input
Point Gerald's avatar
Point Gerald committed
226
227
      stream is indicated either by an end-of-file character (e.g ^D) or by an
      explicit keyword given as parameter (default=EOF).
Point Gerald's avatar
Point Gerald committed
228
229
230
- 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 
Point Gerald's avatar
Point Gerald committed
231
      time of ARC commands
Point Gerald's avatar
Point Gerald committed
232
233
234
- AND assertions are automatically splitted
- store reduced CA into its source CA- 
- Compute minimal cutsets- Use wdd to compute them applying A.Rauzy 
Point Gerald's avatar
Point Gerald committed
235
      algorithm.
Point Gerald's avatar
Point Gerald committed
236
237
238
239
- 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 
Point Gerald's avatar
Point Gerald committed
240
      create lists of variables, ar_dd_project_on_variables with relabelling
Point Gerald's avatar
Point Gerald committed
241
- tests now don't use anymore installed ARC but the one compiled 
Point Gerald's avatar
Point Gerald committed
242
      ${top_builddir}/src
Point Gerald's avatar
Point Gerald committed
243
- integrate CCL into ARC package- The library is automatically downloaded 
Point Gerald's avatar
Point Gerald committed
244
      from GIT repository when bootstrap.sh script is invocated.
Point Gerald's avatar
Point Gerald committed
245
246
247
- 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 
Point Gerald's avatar
Point Gerald committed
248
      expr2dd function
Point Gerald's avatar
Point Gerald committed
249
250
251
- 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 
Point Gerald's avatar
Point Gerald committed
252
      S \subseteq post(S).
Point Gerald's avatar
Point Gerald committed
253
- 'symbolically' keyword is now the default for acheck specifications- 
Point Gerald's avatar
Point Gerald committed
254
      'exhaustively' must be used to use explicit graph.
Point Gerald's avatar
Point Gerald committed
255

Point Gerald's avatar
Point Gerald committed
256
257
258
  ** 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
Point Gerald's avatar
Point Gerald committed
259
      events of that node.
Point Gerald's avatar
Point Gerald committed
260
261
262
- 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 
Point Gerald's avatar
Point Gerald committed
263
      non-interactive mode
Point Gerald's avatar
Point Gerald committed
264
- change shell parser to return asap in order to prevent stack-overflow in
Point Gerald's avatar
Point Gerald committed
265
      yyparse    
Point Gerald's avatar
Point Gerald committed
266
267
- fix error in indexation of quantified variables.
- fix memory leak in computation of reachables- global assertion wasn't 
Point Gerald's avatar
Point Gerald committed
268
      unreferenced.
Point Gerald's avatar
Point Gerald committed
269
270
271
- minor fix in shell grammar.
- composite variables were not correctly flatten.
- in enumeration of paths when displaying the DD solutions- For DD=one 
Point Gerald's avatar
Point Gerald committed
272
      nothing was displayed.
Point Gerald's avatar
Point Gerald committed
273
- #31: array containing post_conditions was not computed prior the 
Point Gerald's avatar
Point Gerald committed
274
      computation of pre-defined sets.
Point Gerald's avatar
Point Gerald committed
275
276
277
- #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 
Point Gerald's avatar
Point Gerald committed
278
      made only on the 1st assertion.
Point Gerald's avatar
Point Gerald committed
279
- fix stack overflow in shell parser-    
Point Gerald's avatar
Point Gerald committed
280

Point Gerald's avatar
Point Gerald committed
281
282
283
* arc 1.3.5
** Bug fixes
- update install-arc.sh
284

Point Gerald's avatar
Point Gerald committed
285
286
287
* 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
288

Point Gerald's avatar
Point Gerald committed
289
290
291
* arc 1.3.3
** Bug fixes
- fix bug in symbolic "quot"
Point Gerald's avatar
Point Gerald committed
292

Point Gerald's avatar
Point Gerald committed
293
294
295
* arc 1.3.2
** Bug fixes
- fix a bug related to parameter instanciation
Point Gerald's avatar
Point Gerald committed
296

Point Gerald's avatar
Point Gerald committed
297
298
299
300
301
302
* 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
303

Point Gerald's avatar
Point Gerald committed
304
305
306
307
308
309
310
311
312
313
314
315
316
317
* 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.
point's avatar
point committed
318

Point Gerald's avatar
Point Gerald committed
319
320
321
322
323
324
325
326
327
328
** 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.
point's avatar
point committed
329

Point Gerald's avatar
Point Gerald committed
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
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
* 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.
point's avatar
update    
point committed
382

Point Gerald's avatar
Point Gerald committed
383
384
385
386
** Bug fixing
- in quot, the transitions was not simplified. remove redundant ones.
- error in the project algorithm used by acheck 
- remove several memory leaks