TLA Language syntax

[MK Bug]

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%'

[Stephan Merz]

Please check the documents available from [1] and in particular [2] for descriptions of TLA+ and how to use it. I recommend watching the introductory videos.

Stephan

[1] http://lamport.azurewebsites.net/tla/tla.html
[2] http://lamport.azurewebsites.net/tla/learning.html

> --
> 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+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> 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/16ba99f2-29f3-493d-91bd-e44b9bc72c45%40googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[MK Bug]

Hi Stephan,

I have already seen these links but they are not helpful in writing the specific working I want to achieve. I have been 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

[Martin]

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+u...@googlegroups.com

> <mailto:tlaplus+u...@googlegroups.com>.

> To post to this group, send email to tla...@googlegroups.com

> <mailto:tla...@googlegroups.com>.

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

[Amir A.H.S.A]

You can find everything required to write specifications in the two links that Stephan has kindly provided.

I assume you are trying to specify a method similar to "contains()" method in the Java String class?

In Java you may write this piece of code:
String myString = "abcd";
if(s.contains("abc"))
{
    // do something
}

If we assume that myString corresponds to a sequence in TLA+, then one possible solution of specifying the "contains()" method is to check whether or not the sequence "abc" belongs to the set of all subsequences of myString with length = 3.

I can try and specify the solution for you, but that is no way of solving a problem. You need to try for yourself.

AmirHossein

On Sun, Jun 16, 2019 at 6:55 PM MK Bug <androi...@gmail.com> 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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.

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.

[MK Bug]

Hi Amir,

Yes kind of that. Actually, I want to check a constant must contains some value(this will be must part of the string) along with other values(this could be optional part of the string).

If you can share the working that would be wonderfull.

Regards,
Malaika