[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] How can I define a sequence as part of a record's fields?



Hey Stephan, first off thank you for the timely response. I didn't want to give you a partial response so I've been working through the problem a little bit each day and I gave your suggestion a bit of a go but couldn't seem to figure out where my issue is. I think I should try to create a minimum reproducible example and go from there. 

I was only able to have a state variable as a sequence by declaring the variable seek in VARIABLES and then stating in init:

Init ==
    /\ seek= <<>>  \* i'm able to have a sequence this way, but I'd prefer it in the record as a field
    /\ ...

I tried the following setup:

MyRec == [
    id: recs,
    seek: Seq(Nat)
]

ThingsThatShouldBeTrueAboutMyRec(r) ==
   /\ r.seek= <<>>
   \*/\ r.id... etc.

myrecs = {r \in MyRec : ThingsThatShouldBeTrueAboutMyRec(r) }

I guess I see the issue. If I try to build a set using set comprehension off of an existing set (MyRec), and the cardinality of MyRec can't be determined, its a problem. 

I looked at the help pages, but still am not sure how exactly to override MyRec. How would I represent the sequence as finite/enumerable?

Below is a minimal reproducible example I made, just in case it was unclear what I am trying to do:

-------------------------------- MODULE mre --------------------------------
EXTENDS Sequences
CONSTANTS ID
VARIABLES recs

MyRec == [
    id: ID,     \* ID == {1,2,3}
    seek: <<>>  
]

ShouldBeTrue(m) ==
    /\ m.id \in ID \*should be trivially true bc of record definition?
    /\ m.seek = <<>> \*I want this to be "initialized" to an empty sequence    

Init ==
    /\ recs = {m \in MyRec: ShouldBeTrue(m)}
   
Next ==
    \/ \E rec \in recs:
        rec' = [rec EXCEPT !.seek = Append(@, "value")] \* Add to queue
    \/ \E rec \in recs:
        rec' = [rec EXCEPT !.seek = SubSeq(@, 2, Len(@))] \* Pop the head off
       
Spec == Init /\ [][Next]_recs
=============================================================================

On Thursday, December 1, 2022 at 1:51:27 AM UTC-5 Stephan Merz wrote:
Your definition is perfectly fine: it defines a set of records with two fields, the second of which is a sequence. However, as the error message indicates, TLC cannot evaluate this operator because the set of these records is infinite (it may contain sequences of arbitrary length). Whether this is a problem or not depends on how you intend to use the operator:

- If it only appears in an invariant, say you write "rec \in MyRec" to check that some variable always takes values in this set, then TLC will be able to evaluate this predicate (it doesn't have to enumerate the entire set MyRec to do so).

- If it appears in the definition of the transition system, say your initial condition has a conjunct "rec \in MyRec" or your next-state relation contains "rec' \in MyRec" then indeed your state space can be infinite because the variable can take an arbitrary value in an infinite set, and TLC will not be able to generate the state space. In that case, you can override the definition of MyRec for TLC and restrict the allowed sequences to a finite set (restricting to fixed maximal length), and check a finite subset of the state space. See the corresponding help pages in the Toolbox.

From what you write, it appears that you'll initialize the variable deterministically, so you'll write something like

Init == rec = [id |-> someValue, seek |-> << >>]

and in that case everything should work fine: MyRec will probably only appear in a (typing) invariant.

Regards,
Stephan

On 1 Dec 2022, at 04:27, Alan Munirji <munir...@xxxxxxxxx> wrote:

From Specifying Systems, I read in section 4.1 that:
"The Sequences module defines the following operators on sequences: 
Seq(S) 

The set of all sequences of elements of the set S. For example, h3, 7i is an element of Seq(Nat)."

I thought then that I could have a sequence as a field of a record by doing:
MyRec == [
    id: recs,
    seek: Seq(Nat)
]

but it doesn't work, stating:

Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn],

but can't enumerate the value of the 'seek' field:

Seq(Nat)


(Eventually, I'd like to initialize this record's seek field to be <<>> in the init state, and then use it to track ordered operations.)


I am very new to TLA+, any help would be so appreciated.



--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4351c96e-420c-40f5-b5b4-5ed42fa131dcn%40googlegroups.com.

--
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/8b21fdc2-fe19-40d4-ab34-52205ce90ad9n%40googlegroups.com.