Possible bug in TLC?

(3 posts) (2 voices)
  • Started 10 months ago by giuliano
  • Latest reply from Leslie Lamport

Tags

No tags yet.

  1. giuliano
    Member

    Hello, I'm having trouble running TLC. I'm using the latest version of the tla tools without the toolbox (just using a terminal on linux).

    Here is a simplified version of my setup:
    -
    I defined two modules, NoCrash and Library, as follows (in two different files):

    ------------------------ MODULE NoCrash ------------------------
EXTENDS Library
CONSTANTS X
VARIABLES y
-----------------------------------
Init == y = TRUE
Z == {h \in MySeqs : \E p \in X : TRUE}
Next == Z = TRUE
==============================
    ------------------------------- MODULE Library  -------------------------------
CONSTANT MySeqs
=====================================

    In order to use TLC I then defined module MCNoCrash as follows:

    -------------------- MODULE MCNoCrash --------------------------------
EXTENDS Library
CONSTANT X
BS == [{1} -> {1}]
VARIABLE y
I == INSTANCE NoCrash
Next == I!Next
Init == I!Init
============================

    And the following configuration file:

    INIT Init
NEXT Next
CONSTANTS
X = {}
MySeqs <- BS

    When running TLC with the command "java -cp ~/tla/tla/ tlc2/TLC MCNoCrash.tla", I get the following output:
    -
    Computing initial states...
    Finished computing initial states: 1 distinct state generated.
    Error: In evaluation, the identifier X is either undefined or not an operator.
    -
    TLC says the error appeared while evaluating the expression "{h \in MySeqs : \E p \in X : TRUE}"
    -
    Although my setup is a bit silly I think I shouldn't get this error. For example if I set BS to the empty set instead of [{1} -> {1}] in module MCNoCrash the error disappears. It also disappears if I replace Z by its definition when defining Next in module NoCrash.

    Is this a bug or am I doing something wrong?

    I also get the same error in another situation involving instantiation.
    -
    Thanks for reading my message,
    Giuliano

    Posted 10 months ago #

  2. giuliano
    Member

    Hello, I simplified a bit the example:
    File Test.tla:

    ------------------------ MODULE Test ------------------------

CONSTANTS X

VARIABLES y

-----------------------------------

Init == y = {}

Z == {z \in [{0} -> {0}] : \E x \in X : FALSE}

Next == y' = Z

==============================

    File MCTest.tla:

    -------------------- MODULE MCTest --------------------------------

X == {}

VARIABLES y 

I == INSTANCE Test 

Next == I!Next
Init == I!Init

============================

    File MCTest.cfg:

    INIT Init
NEXT Next

    Given those files, the command "java -cp ~/tla/tla/ tlc2/TLC MCTest.tla" outputs:

    TLC2 Version 2.03 of 10 March 2011
Running in Model-Checking mode.
Parsing file MCTest.tla
Parsing file Test.tla
Semantic processing of module Test
Semantic processing of module MCTest
Starting... (2011-04-15 10:49:44)
Computing initial states...
Finished computing initial states: 1 distinct state generated.
Error: In evaluation, the identifier X is either undefined or not an operator.
line 11, col 37 to line 11, col 37 of module Test
Error: The behavior up to this point is:
State 1: <Initial predicate>
y = {}

Error: The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 11, column 37 to line 11, column 37 in Test

3 states generated, 1 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 1.
Finished. (2011-04-15 10:49:44)

    Line 11 contains
    Z == {z \in [{0} -> {0}] : \E x \in X : FALSE}

    Posted 10 months ago #

  3. Leslie Lamport
    Key Master

    Thanks for the report. We will check it out.

    Posted 8 months ago #

RSS feed for this topic

Reply

You must log in to post.