Re: [tlaplus] Re: TLA Language syntax

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 <android.ruba@xxxxxxxxx> 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.
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/303697b6-14d6-4368-b734-a2a850defd31%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.