I have written specifications in PlusCal for ph and when I checked the Pluscal algorithm after translation into TLA+ the TLC Model Checker showed the DefualtIntValue. what should I do further to check the temporal property in my specification, kindly guide me thanks. Shahbaz Ahmad Ph.D. Scholar Islamia University Bahawalpur Pakistan.
------------------------------ MODULE
phscale ------------------------------
EXTENDS
Naturals, TLC
(***************************************************************************
--algorithm phscale {
variables
ph \in
1..14; \* pH variable ranging from 1 to 14
classification; \* Variable
to store the classification
{
\* Check for different pH ranges and assign
classification accordingly
if (ph <
1) {
classification:=
"Invalid pH value";
} else {
if (ph <
3) {
classification:=
"Strongly acidic";
} else {
if (ph <
7) {
classification
:= "Moderately acidic";
} else {
if (ph = 7)
{
classification
:= "Neutral";
} else {
if (ph <
8) {
classification
:= "Slightly alkaline";
} else {
if (ph <=
14) {
classification
:= "Moderately alkaline";
} else {
classification
:= "Invalid pH value";
}
} \* end ph <= 14
} \*end ph < 8
} \*end ph = 7
} \*end ph < 7
} \*end ph < 3
} \*
end algorithm
}
***************************************************************************)
\* BEGIN TRANSLATION (chksum(pcal) =
"20ee82a9" /\ chksum(tla) = "8bf955aa")
CONSTANT
defaultInitValue
VARIABLES
ph, classification, pc
vars == << ph, classification, pc >>
Init == (*
Global variables *)
/\ ph \in
1..14
/\
classification = defaultInitValue
/\ pc = "Lbl_1"
Lbl_1 == /\ pc = "Lbl_1"
/\ IF ph < 1
THEN /\ classification' = "Invalid
pH value"
ELSE /\ IF ph < 3
THEN /\ classification' = "Strongly
acidic"
ELSE /\ IF ph < 7
THEN /\ classification' = "Moderately
acidic"
ELSE /\ IF ph = 7
THEN /\ classification' = "Neutral"
ELSE /\ IF ph < 8
THEN /\ classification' = "Slightly
alkaline"
ELSE /\ IF ph <= 14
THEN /\ classification' = "Moderately
alkaline"
ELSE /\ classification' = "Invalid
pH value"
/\ pc' = "Done"
/\ ph' =
ph
(* Allow infinite stuttering to prevent deadlock on
termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
Next == Lbl_1
\/
Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(pc = "Done")
\* END TRANSLATION
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
.