[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Giulio Salierno <salier...@xxxxxxxxx>*Date*: Thu, 28 Jun 2018 08:13:09 -0700 (PDT)

Dear all,

considering the following snippet of TLA, i can't figure out why the invariant (x = y) is always verified using the model-checking mode while it’s violated during the simulation mode (as i expect). Moreover using the DFS instead of BFS it's being violated. The invariant should not be eventually violated also during the model-checking execution? I expect that exist in some behavior a state in which x != y.

Thank you

---------------------------- MODULE RandomCheck ----------------------------

EXTENDS TLC,Integers

VARIABLE x,y

Init == /\ x = 0

/\ y = 0

Next == /\ x' = RandomElement(-1..1)

/\ y' = RandomElement(-1..1)

/\ PrintT(x)

/\ PrintT(y)

Invariant == x = y

considering the following snippet of TLA, i can't figure out why the invariant (x = y) is always verified using the model-checking mode while it’s violated during the simulation mode (as i expect). Moreover using the DFS instead of BFS it's being violated. The invariant should not be eventually violated also during the model-checking execution? I expect that exist in some behavior a state in which x != y.

Thank you

---------------------------- MODULE RandomCheck ----------------------------

EXTENDS TLC,Integers

VARIABLE x,y

Init == /\ x = 0

/\ y = 0

Next == /\ x' = RandomElement(-1..1)

/\ y' = RandomElement(-1..1)

/\ PrintT(x)

/\ PrintT(y)

Invariant == x = y

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] Comparison between TLA+ and LTL** - Next by Date:
**Re: Different behaviour of RandomElement during model checking and simulation mode** - Previous by thread:
**Re: [tlaplus] Comparison between TLA+ and LTL** - Next by thread:
**Re: [tlaplus] Different behaviour of RandomElement during model checking and simulation mode** - Index(es):