[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] how we can used the temporal properties in PlusCal algorithm and also removed the termination
--algorithm phtest {
variables
ph \in 0..14; \* pH variable ranging from 0 to 14
classification; \* Variable to store the classification
{
\* Check for different pH ranges and assign classification accordingly
if (ph < 0) {
classification := "Invalid pH value";
} else if (ph < 1) {
classification := "Extremely acidic";
} else if (ph < 2) {
classification := "Strongly acidic";
} else if (ph < 3) {
classification := "Acidic";
} else if (ph < 4) {
classification := "Moderately acidic";
} else if (ph < 5) {
classification := "Weakly acidic";
} else if (ph < 6) {
classification := "Slightly acidic";
} else if (ph = 6) {
classification := "Neutral (water)";
} else if (ph < 7) {
classification := "Slightly alkaline";
} else if (ph < 8) {
classification := "Weakly alkaline";
} else if (ph < 9) {
classification := "Alkaline";
} else if (ph < 10) {
classification := "Moderately alkaline";
} else if (ph < 11) {
classification := "Strongly alkaline";
} else if (ph < 12) {
classification := "Very strongly alkaline";
} else if (ph < 13) {
classification := "Extremely alkaline";
} else if (ph <= 14) {
classification := "Super alkaline";
} else {
classification := "Invalid pH value";
}
}
}
***************************************************************************)
\* BEGIN TRANSLATION (chksum(pcal) = "9e2cb1d6" /\ chksum(tla) = "1fb859e2")
CONSTANT defaultInitValue
VARIABLES ph, classification, pc
vars == << ph, classification, pc >>
Init == (* Global variables *)
/\ ph \in 0..14
/\ classification = defaultInitValue
/\ pc = "Lbl_1"
Lbl_1 == /\ pc = "Lbl_1"
/\ IF ph < 0
THEN /\ classification' = "Invalid pH value"
ELSE /\ IF ph < 1
THEN /\ classification' = "Extremely acidic"
ELSE /\ IF ph < 2
THEN /\ classification' = "Strongly acidic"
ELSE /\ IF ph < 3
THEN /\ classification' = "Acidic"
ELSE /\ IF ph < 4
THEN /\ classification' = "Moderately acidic"
ELSE /\ IF ph < 5
THEN /\ classification' = "Weakly acidic"
ELSE /\ IF ph < 6
THEN /\ classification' = "Slightly acidic"
ELSE /\ IF ph = 6
THEN /\ classification' = "Neutral (water)"
ELSE /\ IF ph < 7
THEN /\ classification' = "Slightly alkaline"
ELSE /\ IF ph < 8
THEN /\ classification' = "Weakly alkaline"
ELSE /\ IF ph < 9
THEN /\ classification' = "Alkaline"
ELSE /\ IF ph < 10
THEN /\ classification' = "Moderately alkaline"
ELSE /\ IF ph < 11
THEN /\ classification' = "Strongly alkaline"
ELSE /\ IF ph < 12
THEN /\ classification' = "Very strongly alkaline"
ELSE /\ IF ph < 13
THEN /\ classification' = "Extremely alkaline"
ELSE /\ IF ph <= 14
THEN /\ classification' = "Super 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")
Kindly guide me regarding termination , LB1 as well as temporal properties in this spec.
Thanks
Shahbaz Ahmad
ph.D student
--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a392adaa-2efa-4ff2-afab-395e5be44a4en%40googlegroups.com.