Confirmation of sequence of execution in model

[fwefew 4t4tg]

Consider this fragment,

process Worker \in 1..MaxProcesses

begin

    i1: call enq(self);

    i2: call deq();

    i3: call enq(self);

    i4: call deq();  

    i5: print << MessageLog >>;

end process;

Am I correct in intepreting this code to mean that the process runs the statement

i1, then i2, … then i5? MaxProcesses = 2, a global.

I ask because there are 10s and 10s of prints of MessageLog when run when I 

would naively expect 2 only i.e. 2 processes * 1 print/process = 2 prints. 

[7532...@gmail.com]

Based on the conversion to TLA+, the translation makes each labeled statement it's own function and runs them all in parallel ... so how do we get a sequential set of executions?

[Stephan Merz]

I believe Leslie answered your question by pointing you to section 2.3 of the PlusCal manual but posted the reply to another thread. In short, TLC performs a breadth-first search of the state space generated by your algorithm and therefore considers all possible interleaved executions of the processes.

Stephan

> On 1 Mar 2019, at 01:51, 7532...@gmail.com wrote:
>
> Based on the conversion to TLA+, the translation makes each labeled statement it's own function and runs them all in parallel ... so how do we get a sequential set of executions?
>

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

[ret2...@gmail.com]

Stephan, I need did look at Hillel's book, and LL's PlusCal PDF. Quoting from LL's book (https://lamport.azurewebsites.net/tla/p-manual.pdf) pg52:

"An atomic operation of an algorithm consists of all control paths that start at some label l, end at a label, and do not pass through any label. For example, this code sequence ... An action A is said to be enabled in a state s iff it is possible to perform an A action in state s—that is, iff there is some state t such that s → t is an A step. For each atomic operation L of a PlusCal algorithm, the TLA+ translation defines an action L that represents the operation—in other words, where s → t is an L step iff executing operation L in state s can produce state t. We call L an atomic action of the algorithm. A"

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

[Hillel Wayne]

> 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

[fwefew 4t4tg]

Point taken. Thank you.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/cLPoV6BFrIU/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.