Resolving internal choice - handling non-deterministic behaviour

[andredidier]

On the following code, an expected trace is, for example <a,b,a> (and the process then terminates). To explain, we need to understand the parallelism of NFTSimple and ChaosE. After the communication of a, the process NFTSimple can communicate unwanted.1 and unwanted.100 and terminate. The process ChaosE can non-deterministically choose to communicate both unwanted.1 and unwanted.100 or block them on the parallelism with Stop behaviour. The current interpreter behaviour only considers the Stop behaviour of ChaosE, blocking the unwanted events.

I tested on revision 88f896a.

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]

André, our understanding of internal choice is that it may resolve immediately; reducing to either of the left or right branches (referencing D23.4b). So, I'd argue that Stop is a valid behaviour of ChaosE :).

[andredidier]

It's true, @joey-coleman, I'll change the title. It should eventually allow unwanted to be chosen, so it depends on how the interpreter resolves a non-deterministic choice (maybe being fair on choosing either behaviour).

[joey-coleman]

It may be possible to force communication on unwanted by simply reversing the order of the arguments, or "hiding" the Stop in another action (even (Skip;Stop) may be sufficient. Many of the non-det choices in the interpreter are made based on the random number generator, so it is possible to set a seed, but I do not know the details for resolving internal choice. I'll look into it at the next opportunity.

[joey-coleman]

So, I checked the code (relevant code is in ActionInspectionVisitor.java) and there is indeed a call to a RNG that resolves this. The RNG is created (and seeded) in AbstractInspectionVisitor.java, but we have no exposed configuration to change the seed, so the simulator always runs the same sequence of random choices every time.

I'll open a separate enhancement issue for exposing that parameter; otherwise I think this can be closed.