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

Re: [tlaplus] How does TLC know which action is the Init action?

From Specifying Systems: "Formally, we define a behavior to be a sequence of states, where a state is an assignment of values to variables. We specify a system by specifying a set of possible behaviors—the ones representing a correct execution of the system." A spec is a temporal formula, which is true of a behavior if the behavior's initial state matches Init and every step matches Next. For example, in Chapter 2, specifying an "hour clock", the book says:

image.png

On Tue, Oct 24, 2023 at 2:25 AM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
The initial condition is just that: the predicate is only evaluated in the initial state.

Stephan

On 23 Oct 2023, at 22:36, jayaprabhakar k <jayaprabhakar@xxxxxxxxx> wrote:

More questions on the syntax.

For the common form of the spec,

Init == count = 0

Next == count' = count + 1

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

Here, wouldn't the Init state be true only at the initialization, and ever since any next state operation takes place, that modifies count, then Init predicate is false forever.
Then, wouldn't this Spec evaluate to false in every behavior?


On Mon, 23 Oct 2023 at 10:55, jayaprabhakar k <jayaprabhakar@xxxxxxxxx> wrote:
Got it. Thanks.

On Mon, 23 Oct 2023 at 10:07, Hillel Wayne <hwayne@xxxxxxxxx> wrote:

Yup, that's fine, as long as the conjunction of the two predicates fully specifies all variables. So you might do something like

Spec == MachineInit /\ WorldInit /\ [][Next]_vars

Or

Spec == Init /\ DebugInit /\ [][Next]_vars

H

On 10/23/2023 12:03 PM, jayaprabhakar k wrote:
Does that mean, if I have the Spec defined as something like,

Spec == Predicate1 /\ [][Next]_vars /\ WF_vars(Next) /\ Predicate2 
Is it still valid? (Because /\ is commutative)

What are the requirements for a valid init step? For example, any predicate with no unprimed variable. Is that required and is it sufficient? 

Similarly, what if there are two predicates that follow the same requirements, would it be a valid TLA+ spec?

Thanks,
JP


On Mon, 23 Oct 2023 at 02:45, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
TLC parses the temporal formula, Init is a state predicate and Next is the [1] action that appears within the sub formula [][A]_v.

Stephan

[1] Although in TLA+ it is OK to write specifications that contain more complex formulas, such as [][A]_v /\ [][B]_w, TLC only accepts temporal formulas that contain a single sub-formula of that form.


On 23 Oct 2023, at 11:09, jayaprabhakar k <jayaprabhakar@xxxxxxxxx> wrote:

In TLC we can specify the behavioral spec as a temporal formula spec, and that is typically defined as

Spec === Init /\ [][Next]_vars /\ WF_vars(Next)

In this case,
  • How does TLC know Init is the init function? And more specifically, how does it know Init must happen before any Next operation occurs?
  • Is it by the order in which they are defined or by convention like if the name is Init etc?

Thanks,
JP
 

-- 
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/CA%2Bt%3DSiKL660Kjkn-aX13y-BytRqaUTCwXf6asFAO3X54e2vKfA%40mail.gmail.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/80431D21-1526-4D57-88CF-DA5078E43506%40gmail.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/CA%2Bt%3DSi%2Bviw5N8D5-WkHkmw8TRsjZ%2Btexn3ZHimXgk0rso_iJ7g%40mail.gmail.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/4a02b4c1-052e-4bbf-ab2f-ac874eb90723%40gmail.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/CA%2Bt%3DSiJ%2BVgKUw2drRMV0oFkXN%2BAdV6hUEDgQLrgoXBOmozqZeA%40mail.gmail.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/9E16FF02-E5D5-4BF3-AE1A-360F028CB53E%40gmail.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/CAFRUCtZa%2BR2nFj%2BkN5i-bQ%3Dc%2BVZY25TMhsMZ3rvoEK%2BnQ20d0A%40mail.gmail.com.