Re: [tlaplus] Using of PlusCal in smart agriculture to write specification for potential of hydrogen(ph) in soil

On Thu, Mar 21, 2024 at 10:51 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

If you use the Toolbox, it will declare `defaultInitValue’ as a model value. If you use VSCode or the command line and write the configuration file yourself, add the line

defaultInitValue = defaultInitValue

in the CONSTANT section.

What is the temporal property that you want to verify? If it is the Termination property, add

PROPERTY Termination

to the configuration file. You will also want to replace `algorithm’ by `fair algorithm’ for reasons that are explained in the TLA+ background material such as Lamport’s videos or on learntla.com.

Hope this helps,
Stephan

On Mar 21, 2024, at 17:17, Shahbaz Ahmad <shahbaz4426@xxxxxxxxx> wrote:

first thanks to all,

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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a8976058-2295-4f3f-9612-5e11bc28a5c6n%40googlegroups.com.

--
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/F1CE5639-D7DF-4549-A9EF-573B47A76D65%40gmail.com.