locked
Parallel updates in one single step RRS feed

  • Question

  • Hi,

    Does spec explorer support parallel updates like Abstract state machines ?

    I would like to have something equivalent to the following ASM rule:

    rule MyRule =
    par
     x:=0
     y:=1
     z:=2

     ...

    endpar

    Thanks,

    Jamel.

    Tuesday, December 13, 2011 7:41 AM

Answers

  • Hi Jamel,

    I am not familiar with Abstract state machine, but Spec Explorer is based on .NET, so a rule method is not different from an ordinary C# or VB code. If you write x=x+1 and x=x+2 in C# code, actually x will increase by 3.

    I think a proper work-around would be having a wrapper method to judge if there is conflict.

    Can you tell me more about your requirement of having parallel execution?

    Thanks,

    Xiang

    • Marked as answer by Jameleddine Tuesday, January 17, 2012 3:21 AM
    Saturday, January 7, 2012 2:15 PM
    Moderator

All replies

  • Hi Jamel,

    You can write a rule considering all state updates, I do not know if that is "parallel" updates you mean.

    For example:

    [Rule]

    static RuleA()

    {

       x=1;

       y=2;

    }

    Friday, January 6, 2012 2:55 PM
    Moderator
  • Thanks Xiang for the answer.

    By parallel updates, I'm referring to the concurrent execution of the statements x=1 and y=2. For example the following should lead to no state update since there is a conflict when the two statements are executed concurrently (variable x cannot be updated ):

    x = x+1;
    x:= x+2;

    Thanks,
    Jamel.

    Hi Jamel,

    You can write a rule considering all state updates, I do not know if that is "parallel" updates you mean.

    For example:

    [Rule]

    static RuleA()

    {

       x=1;

       y=2;

    }


    Friday, January 6, 2012 3:26 PM
  • Hi Jamel,

    I am not familiar with Abstract state machine, but Spec Explorer is based on .NET, so a rule method is not different from an ordinary C# or VB code. If you write x=x+1 and x=x+2 in C# code, actually x will increase by 3.

    I think a proper work-around would be having a wrapper method to judge if there is conflict.

    Can you tell me more about your requirement of having parallel execution?

    Thanks,

    Xiang

    • Marked as answer by Jameleddine Tuesday, January 17, 2012 3:21 AM
    Saturday, January 7, 2012 2:15 PM
    Moderator
  • Thanks Xiang.

    Suppose that I have the following simple model:

    static class ModelProgram
        {
            static int s1 = 0;
            static int s2 = 0;

            [Rule(Action = "Rule1()")]
            static void Rule1()
            {
                s1 = 1;
                s1 = 5;
                s2 = 2;
            }

    }

    This model yields two states (0,0) and (5,2). If the three statements s1=1, s1=5 and s2=2 have been executed in parallel in one atomic step, it won't lead to a next state because of the conflict between s1=1 and s1=5.

    Would you please let me know how can I write a wrapper to check that s1 has been updated twice and prevent the transition to take place.

    Thanks,

    Jamel.

    Tuesday, January 17, 2012 5:27 AM
  • Hi Jameleddine,

    Another idea could be (if your intention is to reduce side effects from imperative programming) to translate your statements to constraints:
    Replacing:

    x = x+1;
    //x = x+2;

    with

    static int AddSome(int x)
    {
        var y = Microsoft.Xrt.Runtime.RuntimeSupport.Value<int>();
         
        Condition.IsTrue(y == x + 1);
        //Condition.IsTrue(y == x + 2);
               
        return (y);
    }

    Used e.g. in

    [Rule]
    static int AddRule(int x)
    {
        // Return variable. 
        var y = Microsoft.Xrt.Runtime.RuntimeSupport.Value<int>();

              
        y = AddSome(x);

        // Expand everything, and explore just one case.
        Combination.Pairwise(1, 1);
        Combination.Expand(y);
        Combination.Expand(x);
        return (y);
    }

    “AddRule” will not execute, if “y==x+2” is included.
    This works now like a declarative programming language.
    It has some other difficulties - debugging it etc.
    Much better would be to try to merge AsmL with Spec Explorer.
    I think it would be very smart to model with it our domain, but had no time to try this so far.

    However, hope this helps somehow

    Thursday, February 9, 2012 8:48 AM