1
2
3
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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
From v1.2 to v1.3
-----------------
* New features:
o DFA and GTA package documentation and examples
o in_state_space (in WS2S: to test state space)
o execute (compiles without conjoining)
o pconst (Presburger constants)
o inherited-acceptance analysis (in WS2S: state analysis)
o gta2dot for visualizing GTAs
o C-style comments (/* .. */)
* Bug fixes:
o occasionally wrong free variables read by import
o occasionally non-minimum counter-example
o GTA bug (rare error occurring with huge GTAs)
o recursion on restrictions was not implemented correctly
* Source-code improvements:
o interfaces to DFA and GTA packages simplified
o all memory leaks removed
o improved Emacs MONA mode
o guide/universe construction rewritten
o improved automaton file format
o all timers now use CPU time
o DAG code simplified
* Minor changes:
o unrestriction now explicit (-u option)
o command-line usage now more intuitive
o alphabet now consists of all globally declared variables
o restr-feature removed (was confusing)
o use ws1s, ws2s instead of linear, tree
From v1.3 to v1.4
-----------------
* New features:
o recursive types for WS2S - this feature allows GTA guides to
be specified using a high-level notation, thereby making
tree-mode easier to use and more efficient (- this extension
of MONA makes the FIDO tool almost superfluous, so no more
development will be made on FIDO)
o formula reductions - before the translation into automata,
some reduction techniques are applied, which often reduce
translation time (experiments show 5-70% improvement!)
o new M2L-Str emulation - now the skeleton is specified using a
second-order variable instead of a first-order variable (for
compatibility, the old technique is still available using the
-m option)
* Bug fixes:
o root in WS2S had wrong encoding
o all var1 globals are now asserted first-order even if not used
o export and lastpos didn't work together
o let had wrong scope
o small bugs in GTA and DFA analysis fixed
o the last memory leaks removed (this time we mean it :-)
o occasionally wrong free variables at "where"
o "include" didn't work properly
* Source-code improvements:
o better DAGification (typical 10% time improvement)
o the notions of implicative and conjunctive automata (which
became obsolete when restrictions were added) have been removed
* Minor changes:
o better Graphviz DAG dump
o option -xw added: outputs resulting automaton in external format
o progress information extended: current number of automata in
memory is now shown
|
