I Modified the program with your suggestions , but TLC model checker
shows 2 error ( provide value for constant lower and upper ) .
This is normal behavior. but
when i trying to add values for lower and upper , it will not working.
Double-click on the constant you want to fix and enter the value in the form that opens, as an "ordinary assignment" (default), then click "Finish". Repeat for the other constant.
Then click on the little "+" sign next to "Invariants" and add the formulas you wish to verify.
Finally, click on the triangle in a green circle at the top left of the pane to run TLC.
I believe you may want to watch some of the introductory videos [1] or peruse the Hyperbook [2] before writing and verifying your own specifications.
Regards, Stephan
Pls help regards Renjith S On Tue, Jul 24, 2018 at 12:45 PM, Stephan Merz < stepha...@xxxxxxxxx> wrote: Hello,
could you please be a bit more specific what you mean by "execution errors"?
Once you add a suitable module header and footer (which you appear to have
done judging from the LaTeX translation included with your posting), the
input is syntactically correct.
There are at least two strange aspects to your spec: the second last
conjunct of action Pick constrains the value of i in the state before the
transition, and action Max leaves the value of j' unspecified. TLC will
complain about the second issue. I also find it strange that the initial
values for i and j fixed by the initial condition are discarded in the Pick
action.
Below is a TLA+ module that describes the algorithm that you are apparently
trying to specify, in a somewhat more direct fashion. You can create a
model, indicate integer values for the constant parameters lower and upper
(say, -30 and 30), and check the invariants TypeOK and Correctness. (Disable
the default check for deadlock checking in a sequential program such as this
one.)
Best regards,
Stephan
------------------------------- MODULE maxof2
-------------------------------
EXTENDS Integers
CONSTANTS lower, upper
ASSUME lower \in Int /\ upper \in Int /\ lower <= upper
Range == lower .. upper
null == CHOOSE x : x \notin Range
VARIABLES i, j, max
Init == /\ i \in Range
/\ j \in Range
/\ max = null
Next == /\ max = null
/\ max' = IF i > j THEN i ELSE j
/\ UNCHANGED << i,j >>
TypeOK == /\ i \in Range
/\ j \in Range
/\ max \in Range \cup {null}
Correctness == max # null => max \in {i,j} /\ max >= i /\ max >= j
=============================================================================
On 24 Jul 2018, at 08:31, Renjith Sasidharan <renjit...@xxxxxxxxx> wrote:
Sir,
I m a beginner in TLA+ and my research area is Formal method .While i
m writing a spec in TLA+ , there occurs execution errors. I couldn't
rectify those errors pls correct it. I m attaching the spec also in
PDF
EXTENDS Integers
VARIABLES i,pc,j
Init == (pc="start") /\ (i=0) /\ (j=2)
Pick == \/ /\ pc="start"
/\ i' \in 0..1000
/\ j' \in 2..1002
/\ i = IF i>j THEN i ELSE j
/\ pc'="middle"
Max == \/ /\ pc="middle"
/\ i' = IF i > j THEN i ELSE j
/\ pc'="done"
Next == Pick \/ Max
Regards
renjith S
Dept of CSE
Amrita sChool of Engg
--
You received this message because you are subscribed to the Google Groups
"tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an
email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
<maxof2.tex>
--
You received this message because you are subscribed to the Google Groups
"tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an
email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
-- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx. To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout.
|