Step permutations

Question

Hi,

Got a question on "|||" operator. When I explored this machine, I always got foo(in_good_subject, _) followed by foo(in_bad_subject, _). I thought I would also get foo(in_bad_subject, _) followed by foo(in_good_subject, _).

machine OneInstancePubScenario() : Main where ForExploration = false
{
   let string in_good_subject, string in_bad_subject, MyAdapterImpl conn
      where
      {.
         Condition.In(in_good_subject, "test.FILL.test3");

         Condition.In(in_bad_subject, "a b.c");
      .}
   in

   new conn.MyAdapterImpl;(conn.foo(in_good_subject, _) ||| conn.foo(in_bad_subject, _))
}

machine OneInstancePubProgram() : Main where ForExploration = true
{
   (OneInstancePubScenario;exit) || ModelProgram
}

config Main 
{
    action all MyAdapterImpl;
    
    switch StateBound = 402888;
    switch StepBound = 402888;
    switch PathDepthBound = 402888;
    switch TestClassBase = "vs";
    switch GeneratedTestPath = "..\\TestProject.TestSuite";
    switch GeneratedTestNamespace = "TestProject.TestSuite";
    switch TestEnabled = false;
}

Answer 1

[Splitting the thread, as this question has little to do with the original topic]

Operator ||| just interleaves the steps of two machines in every state. That is, for M1 ||| M2, if both step A from machine M1 and step B from machine M2 are enabled in state S, you will see both steps stemming off S. If what you are after are all permutations of the steps in M1 and M2, you can use operator & instead.

Best,

Nico