Date: Sun, 27 Apr 2008 10:49:39 -0700 (PDT)
From: wii Man

can you please be more precise in your description of:
maybe A not_during B

does it mean:
*)  some A while not B

or does it mean
**)  while B there are no A

Date: Sun, 27 Apr 2008 11:28:00 -0700 (PDT)
From: Michael Igler

I mean something like **)

During the execution of process B there is no execution
of process A allowed.

I think of constraint programming in a sense of temporal aspect.

Date: Sun, 27 Apr 2008 11:46:06 -0700 (PDT)
From: wii Man

I saw the image, however seeing the code would help.
In the past I had written something similar to your example.
I validated concurrency by using an assertion

assert ConcurrentAccessOfA2A4 {
 no a : Action, p1 : Process, p2 : Process
 {
    (p1->A2) in a.next
    (p2->A4) in a.next
 }
}
check ConcurrentAccessOfA2A4 for 3

this would ask Alloy to find a counter example where A2 and A4 are
concurrently executed.  If you don't want the behaviour to take place,
change the assertion into a fact. Example

no a:Action, disj p1,p2:Process | (p1->A2) in a.next && (p2->A4) in a.next

this says that A1 and A2 can not happen at the same time

Another example

  no a : Action, p1 : Process, p2 : Process|  (p1->A2) in a.next => ! (p2->A4) in a.next

in other words, A2 => Not A1

Date: Thu, 15 May 2008 12:50:47 -0400 (EDT)
From: Felix Chang

Hi Michael:

I'm attaching an Alloy4 model that models processes, states,
red arrows, and black arrows as you described.
The model designates a particular state as Start state,
and I model each state as representing a set of "pending"
processes and a set of "done" processes.

Given "State1 --blackA--> State2 --blackB--> State3 --redC--> State4",
you say that {A,B} can all execute in arbitrary order,
but they must all finish before executing C.

So in my model,
State1.done={} and State1.pending={}.
State2.done={} and State2.pending={A}.
State3.done={} and State3.pending={A,B}.
State4.done={A,B,C} and State4.pending={}.

Note that "pending" and "done" are both sets, so there is no
ordering among them.  You can regard State3.pending as {A, B}
or {B,A} since sets are not ordered.  However, since we separate
the processes into either belonging to the pending set
or the done set, that allows us to express the intention
that everything in the done set are different from
things in the pending set.

You should be able to adjust the model as you see fit,
to express the more complicated properties you mentioned above.

I'm attaching both "pro.als" (the Alloy model file)
and "pro.thm" (a visualization theme file that I think looks good for this)

pro.als

pro.thm

Sincerely,
Felix Chang
Alloy4 Developer