Using of PlusCal in smart agriculture to write specification for potential of hydrogen(ph) in soil

[Shahbaz Ahmad]

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 

[Stephan Merz]

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

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

[Shahbaz Ahmad]

thanks for your good response. Ok, I will check and update my specifications.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/F1CE5639-D7DF-4549-A9EF-573B47A76D65%40gmail.com.