1
Vote

12-01-16_1: handling of tuple quantification

description

Running the prover on the THEOREM in Bug.tla produces an
incomprehensible parsing error report and a bug report.  The problem
is apparently caused by the first set constructor in the last IF,
which TLAPS can't handle.  But it should produce a sensible error
message.

----------------------- MODULE Bug -----------------------
EXTENDS Integers, TLC

VARIABLE x
Type == x \in BOOLEAN
Init == x = TRUE

THEOREM Init => Type
BY DEF Type, Init

Inv  ==  

  /\ IF {i \in {1,3,3,3,4} : i > 1} # {4,3}
       THEN Assert(FALSE, "Test (1 Failed")
       ELSE Print("Test 1 ]OK)", TRUE)
      
  /\ IF {<<i, j>> \in {1,2} \X {2,3} : j > i} # {<<1,2>>, <<1,3>>, <<2,3>>}
       THEN Assert(FALSE, "Test 2 Failed")
       ELSE Print("Test 2 OK", TRUE)
===================================================================

file attachments

comments

MartinRie wrote Jan 19, 2015 at 3:06 PM

Added example tla file. Confirmed as still open 2015-01-19.