WildFire Challenge and TLA+ ToolBox

(5 posts) (2 voices)
  • Started 10 months ago by robson
  • Latest reply from robson
  • 1 Members Subscribed To Topic

Tags

  1. robson
    Member

    Hi, I am new to TLA+ and I trying explore WildFire spec in TLA+ ToolBox.
    But, when I open the WildFire.tla and after create a model, It's is reported
    13 errors (Model Overview tab) to "Specify the values of declared constants".
    Can anyone help-me? What is happening.

    Posted 10 months ago #

  2. merz
    Member

    I haven't tried to reproduce what you are describing but it sounds that the toolbox just asks you to provide values for the constant parameters declared in the specification. (Model checking is performed over finite instances of a generic model, and you have to fix the instance you want TLC to analyze.)

    Hope this helps,
    Stephan

    Posted 10 months ago #

  3. robson
    Member

    Hi, I have provided values ​​for the constants and these errors have disappeared.
    But when I run the TLC Model checher other errors appeared.

    I've provided the following values for the constants:

    LS<-{ls1, ls2, ls3} //option: model value
    DataLen<-4
    InitMem <- [x \in Adr |-> AllOnes]
    Adr <-{adr1, adr2, adr3, adr4} //option: model value
    Proc <- {1,2,3}
    ResponseToEnv(a,b,c,d) <- {<<aInt, aInt', CHOOSE p \in Proc : TRUE, CHOOSE r \in Response:TRUE>>}
    RequestFromEnv(e, f, g, h) <- {<<aInt, aInt', CHOOSE p \in Proc : TRUE, CHOOSE r \in Request:TRUE>>}
    AdrLS(a) <- [x \in Adr |-> ls1]
    ProcLS <- [x \in Proc |-> ls1]

    The TLC report the errors:

    TLC attempted to evaluate an unbounded CHOOSE.
    Make sure that the expression is of form CHOOSE x \in S: P(x).
    line 309, col 13 to line 309, col 36 of module Wildfire
    The error occurred when TLC was evaluating the nested
    expressions at the following positions:
    0. Line 1055, column 44 to line 1055, column 51 in Wildfire

    Posted 10 months ago #

  4. merz
    Member

    Hi,

    indeed TLC cannot evaluate unbounded CHOOSE expressions, i.e. CHOOSE x: P(x). See the TLC documentation: only bounded quantification over finite sets is supported, such as \A x \in S: P(x) or CHOOSE x \in S: P(x), where S is a finite set.

    By the way, Wildfire was not originally intended for model checking -- you would have to rewrite the model to make it amenable to (finite-state) model checking.

    Best regards,

    Stephan

    Posted 10 months ago #

  5. robson
    Member

    Hi Stephan,
    thanks for you help. I'll check this more carefully.

    Posted 10 months ago #

RSS feed for this topic

Reply

You must log in to post.