This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 428 - inconsistency: Expression of type (constraint) cannot be used as a guard
Summary: inconsistency: Expression of type (constraint) cannot be used as a guard
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: GUI (show other bugs)
Version: 4.0.6
Hardware: PC Linux
: P2 trivial
Assignee: Alexandre David
Depends on:
Reported: 2007-10-03 02:21 CEST by Timothy Bourke
Modified: 2008-09-12 13:46 CEST (History)
1 user (show)

See Also:


Note You need to log in before you can comment on or make changes to this bug.
Description Timothy Bourke 2007-10-03 02:21:40 CEST
1) Declare two local variables:
   clock c;
   int b;
2) Add a self-loop transition to the initial state, with the guard:
   b>3 || c<2
3) Run a syntax check: passes.
4) Change the guard to:
   c<2 || b>3
5) Run a syntax check: fails with: Expression of type (constraint) cannot be used as a guard, even though the two guards are logically equivalent and syntactically similar.
Comment 1 Marius Mikučionis 2008-04-25 11:26:16 CEST
The code is quite scattered but formally the typechecker seems to implement the following rules:

invariant ::= integral | (clock "<" clock) | (clock ">" clock) 
          | (clock "<" integer) | (integer ">" clock) 
          | (difference "<" integer) | (integer "<" difference) 
          | (difference ">" integer) | (integer ">" difference)
          | (invariant "&&" invariant) | (integral "||" invariant)

guard ::= invariant | (integer "<" clock) | (clock ">" integer) 
          | (guard "&&" guard) | (integral "||" guard)

constraint ::= guard | (clock "!=" clock) | (clock "!=" integer) 
          | (integer "!=" clock) | (difference "!=" clock)
          | (difference "!=" clock) | "!" constraint | "forall" constraint
          | "exists" constraint | (constraint "&&" constraint) 
          | (constraint "||" constraint)           

Typechecker will try to interpret the expression in simplest possible way (i.e. expression will be invariant if it matches invariant rule, and expression will get promoted to guard only if it cannot match invariant anymore and so on). 

Eventually some expressions might end up as constraints in general, which means  that they are unsupported, they are easily recognized (type CONSTRAINT) and raise "cannot be used as" errors.

As you can see from the rules, the reported problem persists also for invariants.

Having said that, the following additional rules enable typechecker to accept the above expressions:

invariant ::= | (invariant "||" integral)

guard ::= | (guard "||" integral)

This fix has been applied in rev. 3546.
Behold the rest of the code :-)
Comment 2 Timothy Bourke 2008-04-28 03:15:34 CEST
Thanks Marius. I also appreciate your inclusion of the rules.