-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathChangeLog
1031 lines (597 loc) · 30.8 KB
/
ChangeLog
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
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
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
156
157
158
159
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
197
198
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
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
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
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
319
320
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
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
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
2019-03-08 Marius MikuÄionis <marius@cs.aau.dk>
* : utap: fixed FP usage detection for function calls
2019-03-06 Marius MikuÄionis <marius@cs.aau.dk>
* : build: options and scripts for compiling on mac. Mac uses '@'
character in linker flags so it confuses the scripts, thus I changed
all the option files to use '|' instead of '@' ('|' is unlikely to
be used by anyone due to its connotation with a pipe in shell).
2018-12-21 Marius MikuÄionis <marius@cs.aau.dk>
* : engine: added many distributions to sample from: arcsine, beta,
gamma, poisson, weibull, tri (triangular)
2018-12-17 Marius MikuÄionis <marius@cs.aau.dk>
* : engine: added override for all virtual methods
2018-06-08 Marius MikuÄionis <marius@cs.aau.dk>
* : SMC: set the default number of runs to 1 in simulate queries (no
need to specify #runs if just one simulation is needed)
2018-06-07 Marius MikuÄionis <marius@cs.aau.dk>
* : SMC: fixed histogram when DoF<1, cleaned up compiler warnings
2018-06-06 Marius MikuÄionis <marius@cs.aau.dk>
* : SMC: refactored the property syntax and added a possibility to
specify the explicit number of runs uniformly, breaks "simulate"
query syntax
2018-04-12 Marius MikuÄionis <marius@cs.aau.dk>
* : fixed some undefined-behavior by refactoring variable-vector API
2018-02-02 Marius MikuÄionis <marius@cs.aau.dk>
* : build: started transitioning to g++-7 with C++17: 64bit target
is fine compiler crashes while building for 32bit
2017-11-09 Marius MikuÄionis <marius@cs.aau.dk>
* : fixed tracer for CORA traces
2017-12-03 Marius MikuÄionis <marius@cs.aau.dk>
* : added many C math functions, plus normal distribution
2017-10-13 Marius MikuÄionis <marius@cs.aau.dk>
* : UTAP: fixed if-then-else grammar to allow unbounded amount of
if-the-else statements in a row added C++11 "override" to virtual
functions and fixed some
2017-06-02 Marius MikuÄionis <marius@cs.aau.dk>
* : UTAP: added embedded queries to XTA format
2017-06-02 Marius MikuÄionis <marius@cs.aau.dk>
* : UTAP: fixed range inclusion check
2016-11-25 Marius MikuÄionis <marius@cs.aau.dk>
* : fixed location problem in grammar and a few warnings
2016-01-07 Marius MikuÄionis <marius@cs.aau.dk>
* : minor cleanup, fixing some warnings
2015-10-05 Marius MikuÄionis <marius@cs.aau.dk>
* : UTAP: clean up from trivial errors and warnings
2015-10-05 Marius MikuÄionis <marius@cs.aau.dk>
* : UTAP: fixed tracer utility to read the new transition format
with selects
2015-04-22 Marius MikuÄionis <marius@cs.aau.dk>
* : utap: fixed parsing of xml files without queries and formulas
with line breaks
2015-03-13 Marius MikuÄionis <marius@cs.aau.dk>
* : build: added windows launcher, changed to console executable
(hopefully there will fewer streange crashes on windows) and other
small fixes
2015-02-20 Marius MikuÄionis <marius@cs.aau.dk>
* : UTAP: disabled "it may be needed to add a guard involving the
target invariant"
2014-09-29 Wei Zhao <zhaow@cs.aau.dk>
* : Rewrote the query list
2014-09-21 Wei Zhao <zhaow@cs.aau.dk>
* : 1) Added tracing for 'probaSimulate', 'probaEChecker',
'compareProbaCheck' and 'MitlProbaChecker' 2) Fixed the bug getting the error location in command line 3) Fixed the bug exporting the queries into the query file
2014-08-08 Marius MikuÄionis <marius@cs.aau.dk>
* : UTAP: fixed some missing functions for SMC and MITL features
2014-07-01 Alexandre David <adavid@cs.aau.dk>
* : Managed to solve Jin's problem.
2014-06-18 Marius MikuÄionis <marius@cs.aau.dk>
* : Engine: updated to libxml2-2.9.1 and added instructions how to
cross-compile boost and libxml2 for win32.
2014-05-22 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Check that dynamic constructs are only used on edges, throw type
error if a template is referenced in a dynamic construct before
being defined, ensure to delete the process variables when they go
out of scope i.e. for sum (t:T)(e) t is only bound for the
expression e
2014-05-21 Wei Zhao <zhaow@cs.aau.dk>
* : The xml format for queries using in command line:
<formula>..</formula> instead of <property> .. </property>
2014-05-19 Wei Zhao <zhaow@cs.aau.dk>
* : Get the functionality of the runtime error for the symbolic
simulator. If a runtime error happens during query verification, the
GUI now understands whether the error happened in the model or in
the query expression. The error message is shown correctly.
2014-04-09 Danny B. Poulsen <dannybp@cs.aau.dk>
* : made plotting of arbitrary clock expressions (guard and
invariants) work
2014-04-09 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Begun changes to fix problem with the dynamic sum
2014-04-09 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Changed parser for mitl. No more /\ and \/
2014-04-09 Danny B. Poulsen <dannybp@cs.aau.dk>
* : removed unused code
2014-04-09 Danny B. Poulsen <dannybp@cs.aau.dk>
* : ; to , in range of MITL formulas
2014-04-01 Alexandre David <adavid@cs.aau.dk>
* : Some cleanups. Changed use of hybrid. UPPAAL now works on PTA
too. Fixed pb with extrapolation for PTA.
2014-03-24 Alexandre David <adavid@cs.aau.dk>
* : Updated expression_t::isTrue().
2014-03-17 Wei Zhao <zhaow@cs.aau.dk>
* : Added new functions to catch the runtime error for the symbolic
simulator and verifier. Changed the function to print the output
line on the terminal for reading queries from the model xml or the
query file. Fixed the bug when showing the problems in the problem
table in the editor of the GUI.
2014-02-04 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Ensure dynamic templates are only used with SMC properties
2014-02-03 Marius MikuÄionis <marius@cs.aau.dk>
* : updated keyword highlighting
2014-01-27 Danny B. Poulsen <dannybp@cs.aau.dk>
* : removed unused iterator
2014-01-27 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Check that dynamic process variables are indeed known - segfault
could occur before if the Template the process variable was
associated to was not a dynamic template.
2014-01-22 Danny B. Poulsen <dannybp@cs.aau.dk>
* : corrected typecheck for dynamic processes
2014-01-09 Wei Zhao <zhaow@cs.aau.dk>
* : Added comment and remove unuse code
2014-01-09 Wei Zhao <zhaow@cs.aau.dk>
* : Changed the verifier in server. It can read the queries from the
xml file (Open: Output printed on the screen)
2013-11-26 Danny B. Poulsen <dannybp@cs.aau.dk>
* : check that result is not NULL, and avoid double invocation of
getDynamicTemplate
2013-11-15 Alexandre David <adavid@cs.aau.dk>
* : Fixed typo. Avoid undefined behavior.
2013-11-15 Alexandre David <adavid@cs.aau.dk>
* : Removed dead code (had a mem leak too). Fixed exception - right
one is thrown. Added a test to guards for cheaper smc.
2013-11-06 Alexandre David <adavid@cs.aau.dk>
* : Fixed keywords.
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : removed commented code
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : check that the templates used in foreach /forall / exists does
exist
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : fix to ensure location han be handled by Dynamic evaluation
expressions
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Plotting: foreach (...) added for dynamic templates
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : added forall to MITL, fixed bugs in dynamic expressions in the
probachecker
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Allowed use of references in instantiation of dynamic templates
(to allow channels as parameters).
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : proper toString for the dynamic expressions
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : dynamic exists
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : More consistent syntax
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : parsing of forall and exists for process bound variables
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : made dynamic systems work with simulate query
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : type check to ensure references are not passed in parameters of
dynamic templates.
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Typecheck of dynamic templates
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : bug fixes - and moved spawning out of virtual machine
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Fixed problem with multiple dynamic templates
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Begun changes to facilitate compilation of dynamic templates
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : creation of spawn expression in utap
2013-10-24 Danny B. Poulsen <dannybp@cs.aau.dk>
* : added dynamic templates to system
2013-10-03 Alexandre David <adavid@cs.aau.dk>
* : Fixed some errors found by clang. Fixed some smc errors linked
to double. Added asserts.
2013-09-24 Zhenkui Zhang <zhzhang@cs.aau.dk>
* : [TIGA-SMC] compile tigasmc quary and transport the result
expression through the Tiga pipeline
2013-08-31 Alexandre David <adavid@cs.aau.dk>
* : The function random is not computable at compile time.
2013-08-22 Alexandre David <adavid@cs.aau.dk>
* : Added support for double. EXPERIMENTAL Changed semantics of
meta. Updated reftests: meta variables are not printed any more,
0,1 printed as false,true when applicable. Some stupid spaces are
also gone.
2013-04-16 Alexandre David <adavid@cs.aau.dk>
* : Fixed bug in VM. Added warning.
2013-03-06 Alexandre David <adavid@cs.aau.dk>
* : Fixed a segfault. At least detect and work-around it. The true
source of the bug has not been fixed.
2013-02-14 Alexandre David <adavid@cs.aau.dk>
* : Fixed parsing of double. Handle exponential rate <= 0. I did
NOT want to do this but sometimes it is difficult to write the
proper guards (may be arbitrary expressions).
2012-12-06 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Changed Syntax for mitl (MITL keyword has been replaced by Pr). Introduced shorthand for box and diamond operator in mitl.
2012-09-24 Alexandre David <adavid@cs.aau.dk>
* : Fixed precedence problem.
2012-08-20 Marius MikuÄionis <marius@cs.aau.dk>
* : fixed some compiler warnings (and some potential bug about
nested function calls: when the outer function is void then it did
not mark its beginning, where its arguments are stored, see
program.cpp)
2012-08-08 Alexandre David <adavid@cs.aau.dk>
* : Added + operator for Ecdar.
2012-05-09 Alexandre David <adavid@cs.aau.dk>
* : Support for sums of clocks.
2012-04-26 Danny B. Poulsen <dannybp@cs.aau.dk>
* : updated type checking of filtered simulate
2012-04-24 Alexandre David <adavid@cs.aau.dk>
* : Fixed pSimulateReach.
2012-04-19 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Filtered simulate query added
2012-04-12 Alexandre David <adavid@cs.aau.dk>
* : Added cos, sin, exp, log, and random.
2012-03-14 Danny B. Poulsen <dannybp@cs.aau.dk>
* : Fixed typechecking of statistical formulas (Pr[<= ](<>...) and
Pr[<=] ([] ...) )- error introduced while implementing Until for
statistical properties
2012-02-29 Alexandre David <adavid@cs.aau.dk>
* : Changed the grammar. The new one is simplified and will not
accept nested tctl formulas any more.
2012-02-23 Alexandre David <adavid@cs.aau.dk>
* : Fixed compilation for mitl engine. Changed type of rates, now
floating point. Desactivated support for ode.
2012-01-13 Alexandre David <adavid@cs.aau.dk>
* : Solved pb with clocks.
2011-12-23 Alexandre David <adavid@cs.aau.dk>
* : Removed some dead code. Added the simulate property. Not
working against the GUI, Marius will fix this.
2011-11-24 Alexandre David <adavid@cs.aau.dk>
* : Fixed bugs in smc. Added XML_PARSE_RECOVER.
2011-10-11 Alexandre David <adavid@cs.aau.dk>
* : Fixed overflow problem against the GUI. No clue why this shows
up only in some version of ecdar and not elsewhere.
2011-09-30 Arrou-Vignod Else <elsa@cs.aau.dk>
* : Added missing ifdef ENABLE_SBML Done by Elsa Arrou-Vignod
2011-09-27 Arrou-Vignod Else <elsa@cs.aau.dk>
* : Changes brought to add SBML translator in utap Done by Elsa
Arrou-Vignod
2011-07-17 Alexandre David <adavid@cs.aau.dk>
* : Work-in-progress of an ugly hack to support double -- to some
extent.
2011-06-01 Alexandre David <adavid@cs.aau.dk>
* : Hacked CSP sync. Work-in-progress, needs to be fixed.
2011-05-27 Peter Bulychev <peter@cs.aau.dk>
* : added branches to XTA format
2011-05-26 Alexandre David <adavid@cs.aau.dk>
* : Fixed wrong non-determinism detection in smc. Fixed parser rule
for rates. Removed wrong exprTrue in parser.
2011-04-26 Marius MikuÄionis <marius@cs.aau.dk>
* : changed + to # for the number of steps in probabilistic queries
2011-01-21 Alexandre David <adavid@cs.aau.dk>
* : remove assert
2011-01-20 Alexandre David <adavid@cs.aau.dk>
* : Removed deprecated asserts.
2011-01-10 Alexandre David <adavid@cs.aau.dk>
* : Added smc checker for Pr(..) >= Pr(..)
2010-12-20 Alexandre David <adavid@cs.aau.dk>
* : Implemented int rates.
2010-12-13 Alexandre David <adavid@cs.aau.dk>
* : Added prop E[time|steps <= value; max_runs](min|max: expr).
2010-11-10 Alexandre David <adavid@cs.aau.dk>
* : Added proper implementations in PrettyPrinter.
2010-11-08 Alexandre David <adavid@cs.aau.dk>
* : Added option.
2010-11-05 Alexandre David <adavid@cs.aau.dk>
* : Activated lsc syntax. Added histogram generation.
2010-11-01 Alexandre David <adavid@cs.aau.dk>
* : Enabled some LSC parts by default.
2010-10-20 Alexandre David <adavid@cs.aau.dk>
* : Implemented statistical model-checker. Still work to be done to
improve and fix some known issues. See FIXME.
2010-08-09 Alexandre David <adavid@cs.aau.dk>
* : Less verbose debug print.
2010-06-03 Alexandre David <adavid@cs.aau.dk>
* : Fixed overflow detection to skip 0.
2010-04-06 Alexandre David <adavid@cs.aau.dk>
* : Fixed bug 486.
2010-03-18 Arild Martin Møller Haugstad <arild@cs.aau.dk>
* : Experimental CMake-based alternative build-system for server
2009-12-09 Alexandre David <adavid@cs.aau.dk>
* : TIGA: Changed syntax for simulation properties. Now it's more a
more natural (A || B) <= C ... kind of syntax. UPPAAL: Added
support for clock constraints on receiving broadcast
synchronizations. The simulators (server) had to be fixed too. The
GUIs are not affected.
2009-11-13 Alexandre David <adavid@cs.aau.dk>
* : Removed explicit enumeration.
2009-11-03 Alexandre David <adavid@cs.aau.dk>
* : Fixed side-effect asserts. Fixed compilation for Windows.
2009-10-20 Alexandre David <adavid@cs.aau.dk>
* : Implemented consistency checking. Updated transition filter for
open systems. Added fed_t::getBounded().
2009-10-05 Alexandre David <adavid@cs.aau.dk>
* : Changed the semantics of simulation games. Now UPPAAL considers
simulation of open systems. When there is a synchronization, it is
typed in the sense that a broadcast sync is different from a binary
sync, which is different from a "half" sync. Simulation is using
the sync label now, taking full advantage of the syntax. The action
label is ignored for simulation checking. Updated test suite to
reflect the syntax change. Bumped version number. Changed internal
coding of the turned-based variable for simulation checking.
Changed syntax of the property, it is now prefixed by "simulation:".
I will add "refinement:" soon. Separated code for the
transitions+successors from the Transition/Successor-Filter files.
The change is now more significant. Added a place holder for a
future copy constructor of TA systems (utap).
2009-09-28 Sandie Balaguer <sandie@cs.aau.dk>
* :
2009-08-26 Alexandre David <adavid@cs.aau.dk>
* : Added a comment in HashTable. Removed dead code and useless
variables.
2009-08-11 Alexandre David <adavid@cs.aau.dk>
* : Fixed bug 469.
2009-06-25 Alexandre David <adavid@cs.aau.dk>
* : Fixed bug 474.
2009-05-14 Alexandre David <adavid@cs.aau.dk>
* : Added support for Gantt charts in the server. Fixed simulation
game: * distinguish (un)controllable actions to duplicate * take into account forced actions
2009-04-25 Arild Martin Møller Haugstad <arild@cs.aau.dk>
* : prob: new query property; Pmax
2009-03-19 Alexandre David <adavid@cs.aau.dk>
* : Fixed assert.
2009-03-18 Alexandre David <adavid@cs.aau.dk>
* : Fixed bug 465.
2009-03-16 Alexandre David <adavid@cs.aau.dk>
* : Added functionality to AbstractJob to store expressions. Added
functionality to ModelChecker to return feedbacks. Added handling
of "sup: list of expr" property (with expr being state predicate
without side-effect or clock constraints or clock names). Fixed
traces for leadsto. This is a theoretical fix since the bug has not
appeared yet. Somewhat updated other checkers to handle the
changes, they may be broken. Added a functionality to the DBM lib
to handle sup properties easily.
2009-03-10 Alexandre David <adavid@cs.aau.dk>
* : Removed previous inf & sup. Started to add support for (new)
sup.
2009-03-03 Alexandre David <adavid@cs.aau.dk>
* : Made possible to print states with federations. Added 'sum' to
the language, same syntax as exists & forall but limited to integer
expressions only. It's very useful in tctl expressions when ranging
over processes.
2009-03-02 Alexandre David <adavid@cs.aau.dk>
* : Removed implementation for Mani's robust reachability algorithm.
2009-01-26 Marius MikuÄionis <marius@cs.aau.dk>
* : fixed C string library header inclusion problem (GCC 4.3
complains)
2008-12-19 Marius MikuÄionis <marius@cs.aau.dk>
* : fixed partially poor performance with many locations in the
model. Fix is trivial, but the parsing performance gain is more
than 2x (according to gprof). This is due to stupid std::list::size
implementation which should be avoided as plague. Next, Symbol::add
in system/Symbol.cpp should be redesigned, which now naively seeks
to the end of the linked list just to add a new sibling.
2008-10-20 Alexandre David <adavid@cs.aau.dk>
* : Extended the typechecker to accept x'==integral instead of
x'==integer. It is a natural extension when considering that bool
and x' expressions have the same range.
2008-10-03 Arild Martin Møller Haugstad <arild@cs.aau.dk>
* : branching edges partially supported in server (with
ENABLE_BRANCHING) Combination with select will not currently work, support for
simulator is missing, and there is a bug in the dot-formatting when
replying to getTransitions. (while the problem with getTransitions is related to the previous
point --- simulator support not yet considerd/implemented --- the
GUI will also call getTransitions at various other points, notably
right after calling modelCheck...)
2008-09-26 Alexandre David <adavid@cs.aau.dk>
* : Extended control_t* to work with default parameters.
2008-09-09 Marius MikuÄionis <marius@cs.aau.dk>
* : removed redundant typedef (warned by g++-4.3.1)
2008-09-05 Alexandre David <adavid@cs.aau.dk>
* : Updated localization.
2008-09-03 Alexandre David <adavid@cs.aau.dk>
* : Starting to localize parser errors. Still need to do some
replacements for parser.cc.
2008-08-01 Alexandre David <adavid@cs.aau.dk>
* : Fixed compilation with i586-mingw32msvc-g++.
2008-07-31 Alexandre David <adavid@cs.aau.dk>
* : Reject clock differences too.
2008-07-31 aymie <aymie@3b6c4bc8-9f06-0410-8197-9f1a2e675645>
* : Changed the location of the mapping of PO Tiga actions to the
compiler and solved some segfault issues.
2008-07-30 Alexandre David <adavid@cs.aau.dk>
* : Fixed a warning in modelchecker.cpp. Fixed parsing of
observations.
2008-07-16 Alexandre David <adavid@cs.aau.dk>
* : Removed AF2, AG2, EG2, and EF2 types of quantifiers. They were
work-in-progress that have been there for too long. Fixed minor
printing bug for control properties. Added properties for PO Tiga.
Added bootstrap code for PO Tiga.
2008-06-11 Alexandre David <adavid@cs.aau.dk>
* : Improved warning message.
2008-04-25 Marius MikuÄionis <marius@cs.aau.dk>
* : attempt to fix bug 428: allow typechecker to accept (guard ||
integral) expressions as (integral || guard) are accepted. Same
applies to invariants.
2008-02-21 Marius MikuÄionis <marius@cs.aau.dk>
* : compilation fix for gcc-3.4.5 (workaround for strchrnul, since
it is not in 3.4.5)
2007-12-12 Alexandre David <adavid@cs.aau.dk>
* : Cleaned-up stop watch detection. Added detection of more
unsupported features in TIGA (priorities + stop watches).
2007-11-29 Alexandre David <adavid@cs.aau.dk>
* : Makefile now uses the xml2-config found by configure.
2007-10-29 Alexandre David <adavid@cs.aau.dk>
* : Added stop watches. Moved mis-used inline declarations in
System.h. The server still needs to be updated for the concrete
simulator. The rest should be fine.
2007-10-04 Marius MikuÄionis <marius@cs.aau.dk>
* : fixed signalflow analyzer for forall and exists expressions
fixed some pedantic C++ warning issues
2007-05-03 Alexandre David <adavid@cs.aau.dk>
* : Implemented Mani's robust reachability algorithm.
2007-04-03 Marius MikuÄionis <marius@cs.aau.dk>
* : fixed signal flow for incompletely partitioned specifications
fixed some gcc-4.1.2 compiler warnings
2007-03-01 John Håkansson <john@it.uu.se>
* : Added syntax-switches for parsing expression-lists and XTA
processes
2007-02-22 Gerd Behrmann <behrmann@cs.aau.dk>
* : Added 'mkdir src/utap', since svn seems to eat the empty
directory.
2007-02-22 Gerd Behrmann <behrmann@cs.aau.dk>
* : - Bumped UTAP version number to 0.91. - Updated Makefile.am for new files - Added automatic ChangeLog generation - Updated NEWS file with changes in 0.91
2007-02-09 Alexandre David <adavid@cs.aau.dk>
* : Extended syntax of control_t*. Fixed bug with -T. Reduced
usage of 'promote' in backward propagation. Changed semantics of
evaluation for control_t* prefix expressions. Removed isConstant
from Expression.
2007-01-29 Alexandre David <adavid@cs.aau.dk>
* : Sync my repository a little more. This is for robust
reachability.
2006-12-22 Gerd Behrmann <behrmann@cs.aau.dk>
* : Fixes bug 372.
2006-12-11 Gerd Behrmann <behrmann@cs.aau.dk>
* : Fixes bug 336.
2006-12-04 Alexandre David <adavid@cs.aau.dk>
* : Added color to uppaal test script. Removed the TIGA_TEST flag
switch, it is always on now. Added an extension for inf: and sup:
properties. Only the parser supports it. Tiga accepts more formulas
but ignores the new path-formula arguments.
2006-11-30 Alexandre David <adavid@cs.aau.dk>
* : - Added option for no option in the setup. - Added syntax extension to support inf & sup parameter: formula. - Fixed SystemClockAccessor to depend on the state since clock mapping may change. - Fixed an ugly leak (uh!) in the strategy and also made the generation faster (no search in the state set for states anymore).
2006-11-17 John Håkansson <john@it.uu.se>
* : introduced StatementBuilder (towards fixing enhancement/bug#120)
Also added a syntax switch, and optional parameter to
'parseProperty'.
2006-11-13 Gerd Behrmann <behrmann@cs.aau.dk>
* : Fixes bug 367 and bug 370, in addition to a few bugs introduced
during the 4.1 development phase.
2006-11-05 Gerd Behrmann <behrmann@cs.aau.dk>
* : Merged changes between rev. 2791 and 2792 from the 4.0 branch.
Fixes bug 352.
2006-11-05 Gerd Behrmann <behrmann@cs.aau.dk>
* : Added commen on how to invoke the script.
2006-11-05 Gerd Behrmann <behrmann@cs.aau.dk>
* : Added test script for pretty printer. Changed invocation of pretty printer. Changed syntax check utility to set return code in case of errors.
2006-10-13 Gerd Behrmann <behrmann@cs.aau.dk>
* : Merged changes from 4.0 branch between rev. 2757 and 2758. Fixes
bug 358.
2006-10-04 Marius MikuÄionis <marius@cs.aau.dk>
* : minor code cleanup, added a few more comments
2006-09-23 Gerd Behrmann <behrmann@cs.aau.dk>
* : Refined side-effect analysis. Fixes bug 348.
2006-08-10 Marius MikuÄionis <marius@cs.aau.dk>
* : rename IO interface into timed automata signal flow
2006-07-18 Marius MikuÄionis <marius@cs.aau.dk>
* : don't add conflicting nodes (neither to IUT nor to Env) increase
color contrast for non-colored printer emphasize the observable
channels with "peripheries=2"
2006-07-14 Gerd Behrmann <behrmann@cs.aau.dk>
* : Further clean up.
2006-07-13 Marius MikuÄionis <marius@cs.aau.dk>
* : added partitioning into Environment and IUT of the system
removed constant expressions from analysis
2006-07-02 Gerd Behrmann <behrmann@cs.aau.dk>
* : Fixed doxygen comments.
2006-07-02 Gerd Behrmann <behrmann@cs.aau.dk>
* : Renamed check utility to syntaxcheck.
2006-06-27 Emanuael Fleury <fleury@cs.aau.dk>
* : Changed the flag ENABLE_GAMES into ENABLE_TIGA
2006-06-21 Emanuael Fleury <fleury@cs.aau.dk>
* : - First step to synthesize safety properties - Added a 'weak until' operator - Added toString support for (weak) until - Checked if utap was not broken with 'make test' - Added win/lose formula extraction - Checked on tiga-reftest that nothing was broken
2006-06-20 Gerd Behrmann <behrmann@cs.aau.dk>
* : Replaced include of stdint.h with inttypes.h on platforms
without stdint.h.
2006-06-20 Alexandre David <adavid@cs.aau.dk>
* : Replaced tabulations by 8 spaces.
2006-06-12 Gerd Behrmann <behrmann@cs.aau.dk>
* : Made TIGA keywords conditional so that they only have effect
with ENABLE_GAMES. Removed print() and atomic() from TCTLExpression.
2006-06-10 Emanuael Fleury <fleury@cs.aau.dk>
* : - Fixed a mis-use of property() for T_CONTROL (my fault) - Released a bit the nesting detector for control formula - Performed a non-regression test (ok) - Removed the comments in keywords.gperf - Adding some pretty printing for CONTROL and A_UNTIL
2006-06-08 Emanuael Fleury <fleury@cs.aau.dk>
* : Committing to synchronize with Alexander.
2006-06-08 Emanuael Fleury <fleury@cs.aau.dk>
* : Fixing some inconsistencies in my way of using #ifdef...
2006-06-08 Emanuael Fleury <fleury@cs.aau.dk>
* : Committing common.h (I forgot to include it last time).
2006-06-07 Gerd Behrmann <behrmann@cs.aau.dk>
* : Added full CTL parsing.
2006-06-02 Alexandre David <adavid@cs.aau.dk>
* : Removed #ifdef ENABLE_GAMES since the addition was
non-intrusive.
2006-06-01 Gerd Behrmann <behrmann@cs.aau.dk>
* : Changed tab to space.
2006-06-01 Gerd Behrmann <behrmann@cs.aau.dk>
* : Changed first line off all files to force emacs to save with
space characters rather than tabs.
2006-05-10 Gerd Behrmann <behrmann@cs.aau.dk>
* : Fixes bug 322.
2006-04-29 Gerd Behrmann <behrmann@cs.aau.dk>
* : Added new tracer utility. No longer depends on UTAP. Uses the
new UPPAAL intermediate format. In constrast to the old tracer
utility, this should work with any UPPAAL model.
2006-03-23 Gerd Behrmann <behrmann@cs.aau.dk>
* : Fixed compilation on Mac OS
2006-03-19 Gerd Behrmann <behrmann@cs.aau.dk>
* : Disallowed initialiser on arrays indexed by scalar set.
2006-03-16 Gerd Behrmann <behrmann@cs.aau.dk>
* : Added type checking for bug 279. Resolves the bug.
2006-03-16 Gerd Behrmann <behrmann@cs.aau.dk>
* : Arrays are now parsed by calling typeArrayOfSize() rather than
providing the dimension as a parameter to declVar() and similar
methods. Towards a fix for bug 279.
2006-03-15 Gerd Behrmann <behrmann@cs.aau.dk>
* : Added RATE type to list of non-prefix types.
2006-03-15 Gerd Behrmann <behrmann@cs.aau.dk>
* : Fixes bug 292 and 293. Removes the interpreter from UTAP. Thus the tracer utility no longer
works, but it should be replaced by a new utility using the Uppaal
compiler output. Started work on a fix for bug 279.
2006-03-09 Gerd Behrmann <behrmann@cs.aau.dk>
* : Removed unused code.
2006-03-08 Gerd Behrmann <behrmann@cs.aau.dk>
* : Incremented version number to Beta1-pre5. (and forgot to check in typechecker.h in prev. rev.)
2006-03-08 Gerd Behrmann <behrmann@cs.aau.dk>
* : Fixed bug that destroyed info about arrays in records.
2006-03-08 Gerd Behrmann <behrmann@cs.aau.dk>
* : Fixed toString() for DOT expressions.
2006-03-05 Gerd Behrmann <behrmann@cs.aau.dk>
* : Removed call-by-reference parameter for increased clarity of
code.
2006-03-05 Gerd Behrmann <behrmann@cs.aau.dk>
* : Changed getSymbol() on function call expressions to return the
symbol of the function.
2006-03-04 Gerd Behrmann <behrmann@cs.aau.dk>
* : Changed syntax for partial instantiation such that a type must
be given for each parameter.
2006-03-03 Gerd Behrmann <behrmann@cs.aau.dk>
* : Extended syntax for partial instantiation of templates.
2006-03-02 John Håkansson <john@it.uu.se>
* : Fixed bug in priorities: thanx Alexandre for finding this.
2006-02-28 Gerd Behrmann <behrmann@cs.aau.dk>
* : Fixed bug in type_t::getSub() (TYPENAME was propagated). Fixed structural equivalence check for == and != operators. Added substitution of process arguments in type of dot expressions
(needed for the structural equivalence check).
2006-02-27 John Håkansson <john@it.uu.se>
* : - Changed the syntax of ChanElement to be a ChanExpression or
T_DEFAULT. - Expressions are type checked to make sure that they indeed resolve
to channels or arrays of channels. - Changed the representation in TimedAutomataSystem to provide a
list of pairs of priority and an expression evaluating to a channel
reference or a reference to an array of channels. - Changed the compiler to retrieve the channel-priority list and
evaluate the expressions to figure our which channel or channels
this priority applies to.
2006-02-23 Gerd Behrmann <behrmann@cs.aau.dk>
* : Added type checking for template set specifications. Allowed
constant scalars in template set specifications. Fixes bug 264.
2006-02-22 John Håkansson <john@it.uu.se>
* : Changed priority syntax to "chan priority" for defining
priorities on channels (changed already in rev 1551)
2006-02-21 Gerd Behrmann <behrmann@cs.aau.dk>
* : Changed representation of primitive types: They now have their
own 'kind' value. Made primitive types like int, bool and clock keywords. Changed
builder interface to simplify how primitive types are processed.
2006-02-21 Gerd Behrmann <behrmann@cs.aau.dk>
* : Replaced use of C strings with STL strings. Fixed a crash bug caused by syntax errors in records.
2006-02-13 John Håkansson <john@it.uu.se>
* : Changed keyword 'chan_priority' to 'priority' and removed #ifdef
ENABLE_PRIORITY
2006-02-11 Gerd Behrmann <behrmann@cs.aau.dk>