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