"Successor state is not completely specified by the next-state action" error

(2 posts) (2 voices)
  • Started 4 months ago by sid_rao
  • Latest reply from hansen
  • 1 Members Subscribed To Topic

  1. sid_rao
    Member

    Hi, I have some experience with TLA+. Currently, I am writing a specification which gives the following error,
    "Error: Successor state is not completely specified by the next-state action."

    The transition function in the model which causes this error is,

    BootRomOp ==
    /\ pc = "rom"
    /\ BootRom_state' = IF (BootRom_corrupt=0)
    THEN "malicious"
    ELSE "good"
    /\ pc' = "boot"
    /\ UNCHANGED <<variables>>
    ---end---

    However, the error goes away and TLC completes successfully, if I remove the "IF THEN ELSE" construct from the above transition function, and reformulate the function as, for example,

    BootRomOp ==
    /\ pc = "rom"
    /\ BootRom_state' = "good"
    /\ pc' = "boot"
    /\ UNCHANGED <<variables>>
    ----end-----

    Can someone give me an insight into why I am getting the "Successor state is not completely specified" error?

    Posted 4 months ago #

  2. hansen
    Member

    The error is being caused by the precedence of the "IF THEN ELSE" construct. The "ELSE" clause has the lowest possible precedence and ends only after the "UNCHANGED" statement (see Specifying Systems, chapter 15.2.1: Undelimited Constructs). To fix the error you have to put the whole "IF THEN ELSE" construct in brackets: ... BootRom_state' =(IF BootRom_corrupt=0 THEN "malicious" ELSE "good") /\ ...

    Posted 3 months ago #

RSS feed for this topic

Reply

You must log in to post.