Interpreter: process state update error using replicated external choices

[beokrt]

the process cannot syn on the value 1 on channel ch_a, becouse the other process do not offer to sync on channel ch_a with the value 1.hence we have a livelock

But the tool update the process state var to 1, even that the we have sync on ch_a.3. This is the only event we can sync on. hence the guard of process local_stateliveLock becose true and both processes can now skip, this is not right.

channels
ch_a : int
ch_stop

process local_stateliveLock =
begin
state
skipValue:int  := 0

actions
loop = (  [] i in set {1,3}  // this do now work, the value 1 are picked and then the guard become true
             @( ch_a.(i)-> (skipValue := i;loop)
              [] 
               ([skipValue = 1]& ch_stop-> Skip))
      ) //skipvalue can never be 1, since the other process only can send 2n and 3

 loop2 =   // this work, unfolding the set {1,3]
 (  
     ( dcl k:int := 1 @( ch_a.(k)-> (skipValue := k;loop2)[] ([skipValue = 1]& ch_stop-> Skip)))
        []
     ( dcl k:int := 3 @( ch_a.(k)-> (skipValue := k;loop2)[] ([skipValue = 1]& ch_stop-> Skip)))  
  )     
 @ ch_stop->loop   
end

process local_sendliveLock =
begin
actions
   loop = (( [] i in set {2,3}@ ch_a.(i)->loop) [] ch_stop->Skip)
 @  ch_stop->loop 
end

process localdataliveLock_main = local_stateliveLock  [|{|ch_a,ch_stop|}|] local_sendliveLock 

[joey-coleman]

trace: [ ch_stop; ch_a.3 ] Then ch_stop should be refused (i.e. not offered)

[lausdahl]

So it seems that a simpler test that actually crashes the interpreter is (code snippet):

state
skipValue:int  := 0

actions
loop = (  ([] i in set {1,3}\{skipValue}  
             @( ch_a.(i)-> (skipValue := i;loop))
              [] 
               ([skipValue = 1]& ch_stop-> Skip))
      ) 

the result here is:

Top CML behavior: WAITING_EVENT
Waiting for environment on : ch_stop, tock
Executing: ch_stop
Top CML behavior: RUNNING
Waiting for environment on : tau, tau, tock
Waiting for environment on : tau, ch_a.3, tock
Waiting for environment on : ch_a.3, tock, tau, tau
Waiting for environment on : ch_a.3, tau, tock
Waiting for environment on : ch_a.3, ch_a.1, tock
Executing: ch_a.3
Exception in thread "main" java.lang.NullPointerException
            at eu.compassresearch.core.interpreter.CommonInspectionVisitor.syncOnTimeAndJoinChildren(CommonInspectionVisitor.java:76)
            at eu.compassresearch.core.interpreter.CommonInspectionVisitor.caseAExternalChoice(CommonInspectionVisitor.java:321)
            at eu.compassresearch.core.interpreter.ActionInspectionVisitor.caseAExternalChoiceAction(ActionInspectionVisitor.java:383)
            at eu.compassresearch.core.interpreter.ActionInspectionVisitor.caseAExternalChoiceAction(ActionInspectionVisitor.java:85)
            at eu.compassresearch.ast.actions.AExternalChoiceAction.apply(AExternalChoiceAction.java:335)
            at eu.compassresearch.core.interpreter.CmlInspectionVisitor.defaultPAction(CmlInspectionVisitor.java:45)
            at eu.compassresearch.core.interpreter.CmlInspectionVisitor.defaultPAction(CmlInspectionVisitor.java:20)
            at eu.compassresearch.ast.analysis.QuestionAnswerCMLAdaptor.caseAExternalChoiceAction(QuestionAnswerCMLAdaptor.java:926)
            at eu.compassresearch.ast.actions.AExternalChoiceAction.apply(AExternalChoiceAction.java:335)
            at eu.compassresearch.core.interpreter.ConcreteCmlBehaviour.performInspection(ConcreteCmlBehaviour.java:357)
            at eu.compassresearch.core.interpreter.ConcreteCmlBehaviour.inspect(ConcreteCmlBehaviour.java:378)
            at eu.compassresearch.core.interpreter.VanillaCmlInterpreter.inspect(VanillaCmlInterpreter.java:321)
            at eu.compassresearch.core.interpreter.VanillaCmlInterpreter.executeTopProcess(VanillaCmlInterpreter.java:292)
            at eu.compassresearch.core.interpreter.VanillaCmlInterpreter.execute(VanillaCmlInterpreter.java:214)

[lausdahl]

I would guess that the initial specification can be changed as follows:

channels
ch_a : int
ch_stop

process local_stateliveLock =
begin
state
skipValue:int  := 0

actions
loop = (  [] i in set {1,3}\{skipValue}  
             @( ch_a.(i)-> (skipValue := i;loop)
              [] 
               ([skipValue = 1]& ch_stop-> Skip))
      )

 @ loop   
end

and then the only valid trace will be (ch_a.3(,ch_a.1)*,ch_stop)|((ch_a.1,)*ch_stop) writting with interpreter test regex

[andredidier]

Maybe the following code is another example of this issue. Note that process ChaosE has a similar construct to a replicated external choice. When I try to run the interpreter for process Lazy_NFTSimple, it crashes (Exception in thread "main" - I couldn't find the stack trace).

types
Unwanted = nat

channels
   a,
   b
   unwanted: Unwanted

values
-- Fault 1: 1
-- Error 1: 100
-- Failure 1: 10000
E = { 1, 100, 10000 }
F = { 1 }

chansets
   Es = {| unwanted.1, unwanted.100, unwanted.10000 |}
   Hs = {| |}

process NFTSimple =
begin
    actions
          NOMINAL_NFTSimple = a -> ((b -> NOMINAL_NFTSimple) [] FAULT_NFTSimple)
          FAULT_NFTSimple = unwanted.1 -> (NOMINAL_NFTSimple [] unwanted.100 -> Skip) 
   @ NOMINAL_NFTSimple
end

process ChaosE = 
begin
actions
    Rec = unwanted?id:(id in set E) -> Decision
    Decision = Stop |~| Rec
@ Decision
end

process Lazy_NFTSimple = (NFTSimple [| Es |] ChaosE) \\ (Es union Hs)

[joey-coleman]

@andredidier — we'll get you to recheck that after we've fixed this bug; I'm not entirely sure it's related, but I'm not betting against, either.

[joey-coleman]

We'll need to recheck André's example before actually closing (Kenneth didn't close, I did with a merge into development)

[andredidier]

The example still throws an exception. Maybe I should open a new issue.

[lausdahl]

Yes it is not fixed in the current version of the tool. The clone commit is older and was downstream from a re-write of related parts of the interpreter.

[joey-coleman]

Don't open a new issue yet; let Kenneth and I ping soon :)

[joey-coleman]

Appears to be fixed in 3f3f92e, both for Klaus' original example (the provided examples behave as expected and the various modifications to the behaviour to actually allow skipValue to get the value 1 also seem to work) and for André's later post.

@andredidier please verify that the latest build (it'll be number 51 on the build server, building as I write this, or grab commit cc85799) works for your example. I tested it and received an alternating sequence of synchronisations on a then b. If your example doesn't work quite right, create a new bug for it.

[andredidier]

@joey-coleman, this issue is now solved for me, but the behaviour is not yet as expected. I opened a new issue, #273.