[/] [trunk/] - Rev 54

Filtering Options

Revisions
Search for
Rev Log message Author Age Path
54 Test002 was nondeterministic.
Test007 fell prey to Uppaal Bug #442
tbourke 1761d 00h 28m /trunk/
53 Improve verification by Uppaal. tbourke 1761d 05h 47m /trunk/
52 Improve verification by Uppaal. tbourke 1761d 05h 54m /trunk/
51 Incorporate a sanity check via verification in Uppaal. tbourke 1761d 22h 03m /trunk/
50 Add a regression test framework. tbourke 1762d 02h 28m /trunk/
49 Improvemens ot accuracy of split zone detection. tbourke 1762d 22h 40m /trunk/
48 Bump the version number. tbourke 1833d 23h 55m /trunk/
47 Implement new technique for handling channel arrays. tbourke 1833d 23h 56m /trunk/
46 Rename the xml directory to uppaalxml. tbourke 1834d 18h 12m /trunk/
45 Rename the parse directory to uppaal. tbourke 1834d 18h 15m /trunk/
44 Just after implementing the improved channel array technique.
The code compiles but has not been tested.
tbourke 1834d 18h 20m /trunk/
43 Remove the pos field from expressions. tbourke 1835d 22h 59m /trunk/
42 Make declaration into a functor. tbourke 1835d 23h 47m /trunk/
41 No need for expression to be a functor. tbourke 1835d 23h 49m /trunk/
37 Add files used in the report. tbourke 1836d 01h 35m /trunk/
36 Unexpanded types in selection bindings were causing exceptions. tbourke 1867d 23h 10m /trunk/
35 Fix a nasty bug when combining location invariant expressions with
transition guards: the selection bindings of the transition guard were not
being considered properly leading to improper variable captures by foralls
in the location invariant expression.
tbourke 1874d 02h 47m /trunk/
34 Fix a nasty bug in ClockExprTrans.negate: it was turning invariant forall
bindings into transition exists bindings. But, the invariant is not negated,
so the bindings shouldn't change.

Also tidied up the debugging output. It is more hierarchical now.
tbourke 1874d 18h 54m /trunk/
33 Improve debugging indentation output. tbourke 1875d 00h 34m /trunk/
32 Added warnings for urgent channels leaving locations with invariants
containing clocks as they may lead to `Clock guards are not allowed on
urgent edges' warnings.
tbourke 1875d 02h 06m /trunk/