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

[tlaplus] Re: Refinement Mapping on Partially Ordered Events

    If your partial ordering is modeling "true concurrency" (two events are not ordered if they can be be executed in parallel)  for example in process algebra the process  (a->x->b)|| (c->x->d) can execute a and c in any order but must wait till both have been performed before the x event is performed by both sequential components. If not you can safely skip the rest of the comment.

Using a true concurrent semantics still equates the two processes (a->x->b)|| (c->x->d)  and (a->x->d)|| (c->x->b) which may not be desirable. If you extend the high level spec to include the "location" of events (a1->x1->b1)|| (c2->x2->d2) and now all you have to do is forget the locations in order to retrieve the low level spec.

This may be of no help in you situation but I have found these "located" models useful to map back and forth between automata and Petri net (true concurrent/partial order model) representations of processes.

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/e78d1969-b84d-4baf-9354-9b0b271d5472%40googlegroups.com.