Re: [tlaplus] Re: Confirmation of sequence of execution in model

[Hillel Wayne <hwayne@xxxxxxxxx>]

> What these sources somewhat avoid is the following. Suppose I want to push an element, then wait an arbitrary time, then pop it.
>
> process Worker \in 1..MaxProcesses
> begin
>      i1: call push (10,self);
>      i2: call pop();
> end process;
>
> is just wrong. since i1: and i2: are both enabled TLA can try both.

This is incorrect. i2 is only enabled after i1 "happens". Try 
translating the following:

process a = "a"
  variables foo = FALSE
begin
  A: foo := TRUE;
  B: assert foo;
end process;

If A and B were both enabled at the start, this would raise a model 
error, but it does not.

Also, using procedures is a common beginner antipattern: it's usually 
better to use inlines or macros if you can.

H

> This is wrong too because no time will pass after i1 before i2 because they are done atomically in a single step:
>
> process Worker \in 1..MaxProcesses
> begin
>      i1: call push (10,self);
>          call pop();
> end process;
>
> So what I failed to understand is how to transform this code:
>
> process Worker \in 1..MaxProcesses
> begin
>      i1: call push (10,self);
>      i2: call pop();
> end process;
>
> such that i2 may only start arbitrarily after i1 is done .... i2 needs some sort of await or other condition to hold it until i1 is done. I gather this sort of sync --- different in mind set from plain-jane programming --- is what I'm missing?

--
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.
For more options, visit https://groups.google.com/d/optout.