Hi - Newbee Question

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

  1. groban
    Member

    I am trying to understand both TLA+ and toolbox. I am useing toolbox-64 on windows 7 prof 64bit. I am testing the hourclock example. ok.
    I am changing HCnxt with the following

    'HCnxt == IF hr' # 14 THEN hr+1 ELSE 1'

    This change shouldn't make my theorem incorrect? I am running model checker and it founds no errors.

    Also in the model checker when i am clicking in the header of the column an empty new window with no state graph is presented.

    Finally, when i am trying to lanch model prover (with right click) it creates an error message that doesn't find c:/cygwin/bin. Does the toolbox needs cygwin pre-installed?

    Thanks for your time

    Posted 7 months ago #

  2. Leslie Lamport
    Key Master

    I'm afraid I don't know what you're trying to do. The definition

    HCnxt == IF hr' # 14 THEN hr+1 ELSE 1

    makes no sense if HCnxt is supposed to be the next-state action. A formula should assert a meaningful sentence. For example, 2+2=4 says "two plus two equals four". Your definition of HCnxt is a formula that says

    If the value of hr in the next state does not equal 14, then the value
    of hr plus 1, else 1.

    That is not a meaningful sentence.

    If we are to figure out the problem you're having with the Toolbox, you will have to describe more precisely what you want to happen and exactly what you have done.

    Posted 1 month ago #

  3. Leslie Lamport
    Key Master

    I'm sorry that my reply was hard to read. Let's see if I can get this to be formatted in a reasonable way.

    I'm afraid I don't know what you're trying to do. The definition

    HCnxt == IF hr' # 14 THEN hr+1 ELSE 1

    makes no sense if HCnxt is supposed to be the next-state action. A formula should assert a meaningful sentence. For example, 2+2=4 says "two plus two equals four". Your definition of HCnxt is a formula that says

    If the value of hr in the next state does not equal 14, then the value
    of hr plus 1, else 1.

    That is not a meaningful sentence.

    If we are to figure out the problem you're having with the Toolbox, you will have to describe more precisely what you want to happen and exactly what you have done.

    Posted 1 month ago #

  4. groban
    Member

    First of all I want to thank you for your time. I will try express better my questions.

    Question 1.
    In the HourClock example I deliberately modify the statement
    HCnxt == IF hr' # 12 THEN hr+1 ELSE 1
    to the false statement
    HCnxt == IF hr' # 14 THEN hr+1 ELSE 1
    in order to permit variable hr to take values 12,13 and see how the toolbox react and discover that the theorem
    HC => []HCini
    does not longer exist. However, I run the model and I see no difference from the previous example without the modification.

    Question 2.
    This question concerns the toolbox operation. I open toolbox and add the HourClock spec. I right click on the spec and select “Launch Prover…”. I click OK in the next window and an alert message appears saying that “Prover Launch has encountered a problem. The given Cygwin path c:/Cygwin/bin does not exist”
    My question is. I should install Cygwin in order to operate the prove tools included in toolbox?

    Finally, as new in TLA and toolbox I believe that it will be very helpful if there is tutorial (with a specific example-code) on how to write and prove a spec with toolbox (including error explanation etc)

    Thank you again!

    Posted 1 month ago #

RSS feed for this topic

Reply

You must log in to post.