# [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.