Bug 627

Summary: Lower bound clock invariants are ignored
Product: UPPAAL Reporter: Niklas Kirk Mouritzsen <nmouri12>
Component: EngineAssignee: Marius Mikuńćionis <marius>
Status: ASSIGNED ---    
Severity: enhancement CC: adavid, nmouri12, rhje12, ulrik
Priority: P5    
Version: 4.1.19   
Hardware: PC   
OS: Windows 10   
Architecture:
Attachments: A system containing two templates that demonstrates the problem. In both templates the location L2 is reachable where it should not be due to an invariant on location L1.

Description Niklas Kirk Mouritzsen 2016-11-11 15:33:10 CET
Created attachment 306 [details]
A system containing two templates that demonstrates the problem. In both templates the location L2 is reachable where it should not be due to an invariant on location L1.

Lower bound block invariants are ignored both in the simulator and verifier.

We have attached a system containing two templates that demonstrates the problem. In both templates the location L2 is reachable where it should not be due to an invariant on location L1.

UrgentIntialTemplate have the following:
a - A template local clock variable.
L0 - The initial location, which is urgent
L1 - A location with the invariant a > 2
L2 - A location which should not be reachable
L0 has an edge to L1
L1 has an edge to L2

ClockGuardTemplate have the following:
a - A template local clock variable.
L0 - The initial location
L1 - The location with the invariant: a > 2
L2 - A location which should not be reachable
L0 has an edge to L1 with a guard stating that: a < 1
L1 has an edge to L2

The system also contains the following two queries that demonstrates that L2 is reachable in both examples.

E<> UrgnetIntial.L2
E<> ClockGuard.L2

This issue seem to be present on Windows 10, OS X 10.11 "El Capitan", and an unknown Linux distribution (Ulrik Nyman).

The bug occurs in 4.1.19 and 4.1.18. In 4.0.14 the bug does not occur, instead we are simply not allowed to use this invariant and get a syntax error instead.
Comment 1 Niklas Kirk Mouritzsen 2016-11-11 15:59:28 CET
A little further investigation shows that running both queries at the same time will mark both as passed (green), while running them separately will mark the query "E<> ClockGuard.L2" as failed (red). This might be useful.

This has been tested using version 4.1.19 on Windows 10.