-
Notifications
You must be signed in to change notification settings - Fork 9
/
ChangeLog
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 <[email protected]>
* : utap: fixed FP usage detection for function calls
2019-03-06 Marius Mikučionis <[email protected]>
* : 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 <[email protected]>
* : engine: added many distributions to sample from: arcsine, beta,
gamma, poisson, weibull, tri (triangular)
2018-12-17 Marius Mikučionis <[email protected]>
* : engine: added override for all virtual methods
2018-06-08 Marius Mikučionis <[email protected]>
* : 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 <[email protected]>
* : SMC: fixed histogram when DoF<1, cleaned up compiler warnings
2018-06-06 Marius Mikučionis <[email protected]>
* : 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 <[email protected]>
* : fixed some undefined-behavior by refactoring variable-vector API
2018-02-02 Marius Mikučionis <[email protected]>
* : 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 <[email protected]>
* : fixed tracer for CORA traces
2017-12-03 Marius Mikučionis <[email protected]>
* : added many C math functions, plus normal distribution
2017-10-13 Marius Mikučionis <[email protected]>
* : 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 <[email protected]>
* : UTAP: added embedded queries to XTA format
2017-06-02 Marius Mikučionis <[email protected]>
* : UTAP: fixed range inclusion check
2016-11-25 Marius Mikučionis <[email protected]>
* : fixed location problem in grammar and a few warnings
2016-01-07 Marius Mikučionis <[email protected]>
* : minor cleanup, fixing some warnings
2015-10-05 Marius Mikučionis <[email protected]>
* : UTAP: clean up from trivial errors and warnings
2015-10-05 Marius Mikučionis <[email protected]>
* : UTAP: fixed tracer utility to read the new transition format
with selects
2015-04-22 Marius Mikučionis <[email protected]>
* : utap: fixed parsing of xml files without queries and formulas
with line breaks
2015-03-13 Marius Mikučionis <[email protected]>
* : 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 <[email protected]>
* : UTAP: disabled "it may be needed to add a guard involving the
target invariant"
2014-09-29 Wei Zhao <[email protected]>
* : Rewrote the query list
2014-09-21 Wei Zhao <[email protected]>
* : 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 <[email protected]>
* : UTAP: fixed some missing functions for SMC and MITL features
2014-07-01 Alexandre David <[email protected]>
* : Managed to solve Jin's problem.
2014-06-18 Marius Mikučionis <[email protected]>
* : 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 <[email protected]>
* : 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 <[email protected]>
* : The xml format for queries using in command line:
<formula>..</formula> instead of <property> .. </property>
2014-05-19 Wei Zhao <[email protected]>
* : 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 <[email protected]>
* : made plotting of arbitrary clock expressions (guard and
invariants) work
2014-04-09 Danny B. Poulsen <[email protected]>
* : Begun changes to fix problem with the dynamic sum
2014-04-09 Danny B. Poulsen <[email protected]>
* : Changed parser for mitl. No more /\ and \/
2014-04-09 Danny B. Poulsen <[email protected]>
* : removed unused code
2014-04-09 Danny B. Poulsen <[email protected]>
* : ; to , in range of MITL formulas
2014-04-01 Alexandre David <[email protected]>
* : Some cleanups. Changed use of hybrid. UPPAAL now works on PTA
too. Fixed pb with extrapolation for PTA.
2014-03-24 Alexandre David <[email protected]>
* : Updated expression_t::is_true().
2014-03-17 Wei Zhao <[email protected]>
* : 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 <[email protected]>
* : Ensure dynamic templates are only used with SMC properties
2014-02-03 Marius Mikučionis <[email protected]>
* : updated keyword highlighting
2014-01-27 Danny B. Poulsen <[email protected]>
* : removed unused iterator
2014-01-27 Danny B. Poulsen <[email protected]>
* : 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 <[email protected]>
* : corrected typecheck for dynamic processes
2014-01-09 Wei Zhao <[email protected]>
* : Added comment and remove unuse code
2014-01-09 Wei Zhao <[email protected]>
* : 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 <[email protected]>
* : check that result is not NULL, and avoid double invocation of
getDynamicTemplate
2013-11-15 Alexandre David <[email protected]>
* : Fixed typo. Avoid undefined behavior.
2013-11-15 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : Fixed keywords.
2013-10-24 Danny B. Poulsen <[email protected]>
* : removed commented code
2013-10-24 Danny B. Poulsen <[email protected]>
* : check that the templates used in foreach /forall / exists does
exist
2013-10-24 Danny B. Poulsen <[email protected]>
* : fix to ensure location han be handled by Dynamic evaluation
expressions
2013-10-24 Danny B. Poulsen <[email protected]>
* : Plotting: foreach (...) added for dynamic templates
2013-10-24 Danny B. Poulsen <[email protected]>
* : added forall to MITL, fixed bugs in dynamic expressions in the
probachecker
2013-10-24 Danny B. Poulsen <[email protected]>
* : Allowed use of references in instantiation of dynamic templates
(to allow channels as parameters).
2013-10-24 Danny B. Poulsen <[email protected]>
* : proper toString for the dynamic expressions
2013-10-24 Danny B. Poulsen <[email protected]>
* : dynamic exists
2013-10-24 Danny B. Poulsen <[email protected]>
* : More consistent syntax
2013-10-24 Danny B. Poulsen <[email protected]>
* : parsing of forall and exists for process bound variables
2013-10-24 Danny B. Poulsen <[email protected]>
* : made dynamic systems work with simulate query
2013-10-24 Danny B. Poulsen <[email protected]>
* : type check to ensure references are not passed in parameters of
dynamic templates.
2013-10-24 Danny B. Poulsen <[email protected]>
* : Typecheck of dynamic templates
2013-10-24 Danny B. Poulsen <[email protected]>
* : bug fixes - and moved spawning out of virtual machine
2013-10-24 Danny B. Poulsen <[email protected]>
* : Fixed problem with multiple dynamic templates
2013-10-24 Danny B. Poulsen <[email protected]>
* : Begun changes to facilitate compilation of dynamic templates
2013-10-24 Danny B. Poulsen <[email protected]>
* : creation of spawn expression in utap
2013-10-24 Danny B. Poulsen <[email protected]>
* : added dynamic templates to system
2013-10-03 Alexandre David <[email protected]>
* : Fixed some errors found by clang. Fixed some smc errors linked
to double. Added asserts.
2013-09-24 Zhenkui Zhang <[email protected]>
* : [TIGA-SMC] compile tigasmc quary and transport the result
expression through the Tiga pipeline
2013-08-31 Alexandre David <[email protected]>
* : The function random is not computable at compile time.
2013-08-22 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : Fixed bug in VM. Added warning.
2013-03-06 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : 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 <[email protected]>
* : 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 <[email protected]>
* : Fixed precedence problem.
2012-08-20 Marius Mikučionis <[email protected]>
* : 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 <[email protected]>
* : Added + operator for Ecdar.
2012-05-09 Alexandre David <[email protected]>
* : Support for sums of clocks.
2012-04-26 Danny B. Poulsen <[email protected]>
* : updated type checking of filtered simulate
2012-04-24 Alexandre David <[email protected]>
* : Fixed pSimulateReach.
2012-04-19 Danny B. Poulsen <[email protected]>
* : Filtered simulate query added
2012-04-12 Alexandre David <[email protected]>
* : Added cos, sin, exp, log, and random.
2012-03-14 Danny B. Poulsen <[email protected]>
* : Fixed typechecking of statistical formulas (Pr[<= ](<>...) and
Pr[<=] ([] ...) )- error introduced while implementing Until for
statistical properties
2012-02-29 Alexandre David <[email protected]>
* : Changed the grammar. The new one is simplified and will not
accept nested tctl formulas any more.
2012-02-23 Alexandre David <[email protected]>
* : Fixed compilation for mitl engine. Changed type of rates, now
floating point. Desactivated support for ode.
2012-01-13 Alexandre David <[email protected]>
* : Solved pb with clocks.
2011-12-23 Alexandre David <[email protected]>
* : Removed some dead code. Added the simulate property. Not
working against the GUI, Marius will fix this.
2011-11-24 Alexandre David <[email protected]>
* : Fixed bugs in smc. Added XML_PARSE_RECOVER.
2011-10-11 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : Added missing ifdef ENABLE_SBML Done by Elsa Arrou-Vignod
2011-09-27 Arrou-Vignod Else <[email protected]>
* : Changes brought to add SBML translator in utap Done by Elsa
Arrou-Vignod
2011-07-17 Alexandre David <[email protected]>
* : Work-in-progress of an ugly hack to support double -- to some
extent.
2011-06-01 Alexandre David <[email protected]>
* : Hacked CSP sync. Work-in-progress, needs to be fixed.
2011-05-27 Peter Bulychev <[email protected]>
* : added branches to XTA format
2011-05-26 Alexandre David <[email protected]>
* : Fixed wrong non-determinism detection in smc. Fixed parser rule
for rates. Removed wrong exprTrue in parser.
2011-04-26 Marius Mikučionis <[email protected]>
* : changed + to # for the number of steps in probabilistic queries
2011-01-21 Alexandre David <[email protected]>
* : remove assert
2011-01-20 Alexandre David <[email protected]>
* : Removed deprecated asserts.
2011-01-10 Alexandre David <[email protected]>
* : Added smc checker for Pr(..) >= Pr(..)
2010-12-20 Alexandre David <[email protected]>
* : Implemented int rates.
2010-12-13 Alexandre David <[email protected]>
* : Added prop E[time|steps <= value; max_runs](min|max: expr).
2010-11-10 Alexandre David <[email protected]>
* : Added proper implementations in PrettyPrinter.
2010-11-08 Alexandre David <[email protected]>
* : Added option.
2010-11-05 Alexandre David <[email protected]>
* : Activated lsc syntax. Added histogram generation.
2010-11-01 Alexandre David <[email protected]>
* : Enabled some LSC parts by default.
2010-10-20 Alexandre David <[email protected]>
* : Implemented statistical model-checker. Still work to be done to
improve and fix some known issues. See FIXME.
2010-08-09 Alexandre David <[email protected]>
* : Less verbose debug print.
2010-06-03 Alexandre David <[email protected]>
* : Fixed overflow detection to skip 0.
2010-04-06 Alexandre David <[email protected]>
* : Fixed bug 486.
2010-03-18 Arild Martin M�ller Haugstad <[email protected]>
* : Experimental CMake-based alternative build-system for server
2009-12-09 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : Removed explicit enumeration.
2009-11-03 Alexandre David <[email protected]>
* : Fixed side-effect asserts. Fixed compilation for Windows.
2009-10-20 Alexandre David <[email protected]>
* : Implemented consistency checking. Updated transition filter for
open systems. Added fed_t::getBounded().
2009-10-05 Alexandre David <[email protected]>
* : 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 <[email protected]>
* :
2009-08-26 Alexandre David <[email protected]>
* : Added a comment in HashTable. Removed dead code and useless
variables.
2009-08-11 Alexandre David <[email protected]>
* : Fixed bug 469.
2009-06-25 Alexandre David <[email protected]>
* : Fixed bug 474.
2009-05-14 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : prob: new query property; Pmax
2009-03-19 Alexandre David <[email protected]>
* : Fixed assert.
2009-03-18 Alexandre David <[email protected]>
* : Fixed bug 465.
2009-03-16 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : Removed previous inf & sup. Started to add support for (new)
sup.
2009-03-03 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : Removed implementation for Mani's robust reachability algorithm.
2009-01-26 Marius Mikučionis <[email protected]>
* : fixed C string library header inclusion problem (GCC 4.3
complains)
2008-12-19 Marius Mikučionis <[email protected]>
* : 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 <[email protected]>
* : 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 <[email protected]>
* : 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 <[email protected]>
* : Extended control_t* to work with default parameters.
2008-09-09 Marius Mikučionis <[email protected]>
* : removed redundant typedef (warned by g++-4.3.1)
2008-09-05 Alexandre David <[email protected]>
* : Updated localization.
2008-09-03 Alexandre David <[email protected]>
* : Starting to localize parser errors. Still need to do some
replacements for parser.cc.
2008-08-01 Alexandre David <[email protected]>
* : Fixed compilation with i586-mingw32msvc-g++.
2008-07-31 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : Fixed a warning in modelchecker.cpp. Fixed parsing of
observations.
2008-07-16 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : Improved warning message.
2008-04-25 Marius Mikučionis <[email protected]>
* : 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 <[email protected]>
* : compilation fix for gcc-3.4.5 (workaround for strchrnul, since
it is not in 3.4.5)
2007-12-12 Alexandre David <[email protected]>
* : Cleaned-up stop watch detection. Added detection of more
unsupported features in TIGA (priorities + stop watches).
2007-11-29 Alexandre David <[email protected]>
* : Makefile now uses the xml2-config found by configure.
2007-10-29 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : fixed signalflow analyzer for forall and exists expressions
fixed some pedantic C++ warning issues
2007-05-03 Alexandre David <[email protected]>
* : Implemented Mani's robust reachability algorithm.
2007-04-03 Marius Mikučionis <[email protected]>
* : fixed signal flow for incompletely partitioned specifications
fixed some gcc-4.1.2 compiler warnings
2007-03-01 John H�kansson <[email protected]>
* : Added syntax-switches for parsing expression-lists and XTA
processes
2007-02-22 Gerd Behrmann <[email protected]>
* : Added 'mkdir src/utap', since svn seems to eat the empty
directory.
2007-02-22 Gerd Behrmann <[email protected]>
* : - 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 <[email protected]>
* : 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 <[email protected]>
* : Sync my repository a little more. This is for robust
reachability.
2006-12-22 Gerd Behrmann <[email protected]>
* : Fixes bug 372.
2006-12-11 Gerd Behrmann <[email protected]>
* : Fixes bug 336.
2006-12-04 Alexandre David <[email protected]>
* : 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 <[email protected]>
* : - 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 <[email protected]>
* : introduced StatementBuilder (towards fixing enhancement/bug#120)
Also added a syntax switch, and optional parameter to
'parseProperty'.
2006-11-13 Gerd Behrmann <[email protected]>
* : Fixes bug 367 and bug 370, in addition to a few bugs introduced
during the 4.1 development phase.
2006-11-05 Gerd Behrmann <[email protected]>
* : Merged changes between rev. 2791 and 2792 from the 4.0 branch.
Fixes bug 352.
2006-11-05 Gerd Behrmann <[email protected]>
* : Added commen on how to invoke the script.
2006-11-05 Gerd Behrmann <[email protected]>
* : 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 <[email protected]>
* : Merged changes from 4.0 branch between rev. 2757 and 2758. Fixes
bug 358.
2006-10-04 Marius Mikučionis <[email protected]>
* : minor code cleanup, added a few more comments
2006-09-23 Gerd Behrmann <[email protected]>
* : Refined side-effect analysis. Fixes bug 348.
2006-08-10 Marius Mikučionis <[email protected]>
* : rename IO interface into timed automata signal flow
2006-07-18 Marius Mikučionis <[email protected]>
* : 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 <[email protected]>
* : Further clean up.
2006-07-13 Marius Mikučionis <[email protected]>
* : added partitioning into Environment and IUT of the system
removed constant expressions from analysis
2006-07-02 Gerd Behrmann <[email protected]>
* : Fixed doxygen comments.
2006-07-02 Gerd Behrmann <[email protected]>
* : Renamed check utility to syntaxcheck.
2006-06-27 Emanuael Fleury <[email protected]>
* : Changed the flag ENABLE_GAMES into ENABLE_TIGA
2006-06-21 Emanuael Fleury <[email protected]>
* : - 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 <[email protected]>
* : Replaced include of stdint.h with inttypes.h on platforms
without stdint.h.
2006-06-20 Alexandre David <[email protected]>
* : Replaced tabulations by 8 spaces.
2006-06-12 Gerd Behrmann <[email protected]>
* : Made TIGA keywords conditional so that they only have effect
with ENABLE_GAMES. Removed print() and atomic() from TCTLExpression.
2006-06-10 Emanuael Fleury <[email protected]>
* : - 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 <[email protected]>
* : Committing to synchronize with Alexander.
2006-06-08 Emanuael Fleury <[email protected]>
* : Fixing some inconsistencies in my way of using #ifdef...
2006-06-08 Emanuael Fleury <[email protected]>
* : Committing common.h (I forgot to include it last time).
2006-06-07 Gerd Behrmann <[email protected]>
* : Added full CTL parsing.
2006-06-02 Alexandre David <[email protected]>
* : Removed #ifdef ENABLE_GAMES since the addition was
non-intrusive.
2006-06-01 Gerd Behrmann <[email protected]>
* : Changed tab to space.
2006-06-01 Gerd Behrmann <[email protected]>
* : Changed first line off all files to force emacs to save with
space characters rather than tabs.
2006-05-10 Gerd Behrmann <[email protected]>
* : Fixes bug 322.
2006-04-29 Gerd Behrmann <[email protected]>
* : 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 <[email protected]>
* : Fixed compilation on Mac OS
2006-03-19 Gerd Behrmann <[email protected]>
* : Disallowed initialiser on arrays indexed by scalar set.
2006-03-16 Gerd Behrmann <[email protected]>
* : Added type checking for bug 279. Resolves the bug.
2006-03-16 Gerd Behrmann <[email protected]>
* : 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 <[email protected]>
* : Added RATE type to list of non-prefix types.
2006-03-15 Gerd Behrmann <[email protected]>
* : 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 <[email protected]>
* : Removed unused code.
2006-03-08 Gerd Behrmann <[email protected]>
* : Incremented version number to Beta1-pre5. (and forgot to check in typechecker.h in prev. rev.)
2006-03-08 Gerd Behrmann <[email protected]>
* : Fixed bug that destroyed info about arrays in records.
2006-03-08 Gerd Behrmann <[email protected]>
* : Fixed toString() for DOT expressions.
2006-03-05 Gerd Behrmann <[email protected]>
* : Removed call-by-reference parameter for increased clarity of
code.
2006-03-05 Gerd Behrmann <[email protected]>
* : Changed getSymbol() on function call expressions to return the
symbol of the function.
2006-03-04 Gerd Behrmann <[email protected]>
* : Changed syntax for partial instantiation such that a type must
be given for each parameter.
2006-03-03 Gerd Behrmann <[email protected]>
* : Extended syntax for partial instantiation of templates.
2006-03-02 John H�kansson <[email protected]>
* : Fixed bug in priorities: thanx Alexandre for finding this.
2006-02-28 Gerd Behrmann <[email protected]>
* : Fixed bug in type_t::get_sub() (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 <[email protected]>
* : - 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 <[email protected]>
* : Added type checking for template set specifications. Allowed
constant scalars in template set specifications. Fixes bug 264.
2006-02-22 John H�kansson <[email protected]>
* : Changed priority syntax to "chan priority" for defining
priorities on channels (changed already in rev 1551)
2006-02-21 Gerd Behrmann <[email protected]>
* : 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 <[email protected]>
* : Replaced use of C strings with STL strings. Fixed a crash bug caused by syntax errors in records.
2006-02-13 John H�kansson <[email protected]>
* : Changed keyword 'chan_priority' to 'priority' and removed #ifdef
ENABLE_PRIORITY
2006-02-11 Gerd Behrmann <[email protected]>