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.
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.