First Last Prev Next    No search results available      Search page      Enter new bug
Bug#: 428
Product:
Component:
Status: RESOLVED
Resolution: FIXED
Assigned To: Alexandre David <adavid@cs.aau.dk>
Hardware:
OS:
Version:
Priority:
Severity:
Reporter: Timothy Bourke <tbourke@cse.unsw.edu.au>
Add CC:
CC:
Remove selected CCs
URL:
Summary:

Attachment Type Creator Created Size Actions
Create a New Attachment (proposed patch, testcase, etc.) View All

Bug 428 depends on: Show dependency tree
Show dependency graph
Bug 428 blocks:
Votes: 0    Show votes for this bug    Vote for this bug

Additional Comments:







View Bug Activity   |   Format For Printing   |   XML   |   Clone This Bug


Description:   Opened: 2007-10-03 02:21
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 From Marius Mikucionis 2008-04-25 11:26:16 -------
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 From Timothy Bourke 2008-04-28 03:15:34 -------
Thanks Marius. I also appreciate your inclusion of the rules.

First Last Prev Next    No search results available      Search page      Enter new bug