Re: [tlaplus] Re: TLA Language syntax

["'Martin' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

Hello Malaika,

The material Stephan linked, in particular the video course and the book
"Specifying Systems" give a good overview of the basic building blocks of TLA+
specifications. One of the most important ones is the set notation you know from
school mathematics.

Tables as in SQL are not directly part of TLA+ and you to express in terms of
sets or directly in predicate logic. In both cases, you need an actual property
of the value that you would like to check.

For example, you could represent the table as a predicate Table(_,_) with
column1 the first argument of the table. The formula

Prop == \A x \in ID, y \in Data : Table(x,y) /\ MatchesRegex(x, Concat(AnyChar,
Concat(String("abc"), AnyChar))) =>  y = "somevalue"

expresses the property that for all table rows where the column1 argument
matches the given regular expression, the second column contains "somevalue".
The \A, /\ and => operators are those from classical logic: universal
quantification ("for all"), conjunction ("and") and implication ("if ... then").
I have left out the definitions of the ID and Data types and the description of
the actual contents of Table. If you were to model check the property, you would
need to fill in those details.

Please also note that there is no built-in regular expression library. You would
need to define the meaning of MatchesRegex yourself - I just used suggestive
names of how this could look like.

What is also important is that TLA+ allows you to reason more abstractly on your
specification - if you try to use it like a programming language, you will not
be able to model check most of your properties.

I hope this helped a bit but in general I can just reiterate the reading
suggestings that Stephan mentioned - in particular the TLA book explains the
language in detail (and it also contains the syntax definition that you were
looking for).

all the best,
Martin

On 6/16/19 4:25 PM, MK Bug wrote:
> Hi Stephan,
> 
> I have already seen these links but they are not helpful in writing the specific
> working I want to achieve. I have digging out this for days but cannot find it,
> if you know any related helpful material or if you can write the logic that
> would be really helpful. Thanks
> 
> Regards,
> Malaika
> 
> On Saturday, June 15, 2019 at 8:02:36 PM UTC+5, MK Bug wrote:
> 
>     I have to write a logic in TLA but cannot fins its syntax.
> 
>     If I want to check that a constant contains a specific value so how I can
>     achieve this.For the more understanding of my logic I have share a below
>     example
> 
>     Example in SQL:
> 
>     Select * from table where column1 like '%abc%'
> 
> -- 
> 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
> <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>.
> To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx
> <mailto:tlaplus@xxxxxxxxxxxxxxxx>.
> Visit this group at https://groups.google.com/group/tlaplus.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tlaplus/303697b6-14d6-4368-b734-a2a850defd31%40googlegroups.com
> <https://groups.google.com/d/msgid/tlaplus/303697b6-14d6-4368-b734-a2a850defd31%40googlegroups.com?utm_medium=email&utm_source=footer>.
> For more options, visit https://groups.google.com/d/optout.

-- 
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9a38c40c-d7e3-8f11-37b0-c492d32c3102%40gmail.com.
For more options, visit https://groups.google.com/d/optout.