[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus]



Hi,

I want to achieve to check the specific sequence and value in a constant that is character field.
Following is my code
---------------------------- MODULE 06_JUL_2019 ----------------------------

EXTENDS Naturals, TLC,Sequences
CONSTANT email\*,d

(* --algorithm transfer
variables alice_account = 10,  money=1 , Per_Day_Salary = 1000,d \in 1..10;

begin

A: money :=  Per_Day_Salary *d ;
B: alice_account :=  alice_account + money;


end algorithm *)
\* BEGIN TRANSLATION
VARIABLES alice_account, money, Per_Day_Salary, d, pc

vars == << alice_account, money, Per_Day_Salary, d, pc >>

Init == (* Global variables *)
        /\ alice_account = 10
        /\ money = 1
        /\ Per_Day_Salary = 1000
        /\ d \in 1..10
        /\ pc = "A"

A == /\ pc = "A"
     /\ money' = Per_Day_Salary *d
     /\ pc' = "B"
     /\ UNCHANGED << alice_account, Per_Day_Salary, d >>

B == /\ pc = "B"
     /\ alice_account' = alice_account + money
     /\ pc' = "Done"
     /\ UNCHANGED << money, Per_Day_Salary, d >>

Next == A \/ B
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION

Range (seq) == {{seq[i]: i \in 1 .. Len(seq)}\in "ABBC@"}


=============================================================================


-- email is the character field that I am parsing as         "ABC"
--Now want to check if email contains "ABBC@" this sequence. or it could vary like "anyValue@abc" but the specific character must remains the same in this case "@" is the specific character.


Thanks in advance
Malaika

--
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/CA%2BkanUJmYQBdbqfVZMZr593xrmKNjc6QBd0E5QdOQNy--KiQ2w%40mail.gmail.com.