------------------------------ 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