Re: [tlaplus] Could it be possible to check the variable starting alphabet

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Just want to ask how this would be possible with sequence, if you can guide.

It depends on what you consider is important for your specification. Since you are interested in the first and last elements of a sequence of characters, you could let your variable take a sequence of elements, perhaps somewhat as below.

CONSTANT

  Letter,    \* set representing all letters, instantiated for example by a set {a,b,c} of model values

  a, b, c    \* representing individual letters

ASSUME {a,b,c} \subseteq Letter

VARIABLE myletter

Init == myletter = << a,b,a >>

UpdateLetter ==  \* non-deterministically change some letter

  \E i \in 1 .. Len(myletter) : \E l \in Letter : myletter' = [myletter EXCEPT ![i] = l]

GoodLetters ==   \* some state predicate corresponding to desired state

  /\ myletter[1] = a

  /\ myletter[Len(myletter)] = c

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/319FE7BA-6758-44F0-BD3F-BAFD1B40A77D%40gmail.com.