locked
Updating compound value outside of its constructor

    Soru

  • Hi,

    I'm trying to model the well known dining philosophers case study.

    I encountered the following error when trying to explore my program machine:

    Block(ExplorationRuntimeException#0: "Attempt to update field 'DiningPhilosopher.Philosopher.eating' of compound value outside of its constructor. You can only write to compound value fields during construction time.
    Stack trace:
       at DiningPhilosopher.Philosopher.updateEating(System.Boolean)
       at DiningPhilosopher.ModelProgram.StartEating(DiningPhilosopher.Philosopher)
    " Current executing rule method is DiningPhilosopher.ModelProgram.StartEating(DiningPhilosopher.Philosopher)), InCall(<error>)

    Here is my code:

    namespace DiningPhilosopher
    {
        public enum Chopstick {c1, c2, c3, c4, c5};   
        public static class ModelProgram
        {
            static bool Initialized = false;
            static Philosopher Albert = new Philosopher("Albert", Chopstick.c5, Chopstick.c1, false, false);
            static Philosopher Herbert = new Philosopher("Herbert", Chopstick.c1, Chopstick.c2, false, false);
            static Philosopher Fredrich = new Philosopher("Fredrich", Chopstick.c2, Chopstick.c3, false, false);
            static Philosopher Sina = new Philosopher("Sina", Chopstick.c3, Chopstick.c4, false, false);
            static Philosopher Juan = new Philosopher("Juan", Chopstick.c4, Chopstick.c5, false, false);
        
            [Rule(Action = "StartEating(p)")]
            static void StartEating(Philosopher p)
             {
                p.updateEating(true);            
            }
    }

      class Philosopher : CompoundValue
     //class Philosopher
      {       
        public string name;    
        public Chopstick rightChop;
        public Chopstick leftChop;
        public bool eating;
        public bool hungry;
        public Philosopher(string s, Chopstick rc, Chopstick lc, bool eating, bool hungry)
        {
            this.name = s;
            this.rightChop = rc;
            this.leftChop = lc;
            this.eating = eating;
            this.hungry = hungry;
        }
         public void updateEating(bool b)
         {
             this.eating = b;
         }
      }
      
    }

    Would you please help me with this issue.

    Thanks,

    Jamel.

    • Düzenleyen Jameleddine 10 Nisan 2012 Salı 17:55 submit more details
    09 Nisan 2012 Pazartesi 18:34

Yanıtlar

  • Hi Jamel,

    The problem is, that in method updateEating you change an attribute value (eating).
    CompundValue-classes (here Philosopher) do no allow this (they are immutable):
    You must create a brand new one with changed attribute value.

    Here is another idea how you could implement it.
    It uses TypeBinding instead of CompoundValue.

    The dining table is static - a sequence. The philosophers will sit here.
    The philosophers are instance based classes and all completely equal.
    Each has one fork (say left, your agent approach).
    Each can steal a fork from (say right) neighbour (i.e. NeighbourWithFork):

        public static class Room
        {
            public static Sequence<Philosopher> Table = new Sequence<Philosopher>();
            public static Philosopher GetNeighbourWithFork(Philosopher P)
            {
                return (null);
            }
        }
        public enum ForkState { free, grabbed, stolen };
        public enum AgentState { eating, talking };
        [TypeBinding("SpecExplorer1.Sample.ComplexThread")]
        public class Philosopher
        {
            ForkState Fork = ForkState.free;
            AgentState State = AgentState.talking;
            [Rule(Action = "new this.ComplexThread()")]
            Philosopher()
            {
                Room.Table = Room.Table.Add(this);
            }
            [Rule(Action = "this.Step()")]
            void GrabFork()
            {
            }
            [Rule(Action = "this.Step()")]
            void StealFork()
            {
            }
            [Rule(Action = "this.Step()")]
            void StopEating()
            {
            }
        }

    You can copy this and replace the original model code in the instance based example "SimpleThread.cs".
    You get this example, if you create a brand new instance based "SpecExplorer1"-project.

    Already now you can see how two philosophers take a seat at the table in the state browser,
    if you explore machine "SlicedThreadModelProgramm".

    What is left to do:
    * Implementing the rules, which change the state of the philosopher and his neighbour.
      Some examples:
      Grabing a fork is only allowed if fork is not stolen/already grabbed.
      Stealing is only possible if own fork is grabbed/neighbours fork is not already stolen.
      After stealing a fork the philosopher is eating.
    * Using a nice scenario which creates all five philosphers (here Threads from the example):
      machine FiveThreadScenario() : Main
      {
        new ComplexThread{5}; (_* |?| (!call new ComplexThread)*)
      }
    * Mapping the rules on own actions/class in the adapter (at the moment i.e. "ComplexThread.Step")

    Hope this helps.

     


    • Yanıt Olarak Öneren Yiming Cao 11 Nisan 2012 Çarşamba 21:33
    • Yanıt Olarak İşaretleyen Jameleddine 12 Nisan 2012 Perşembe 04:32
    11 Nisan 2012 Çarşamba 15:17

Tüm Yanıtlar

  • Hi Jamel,

    The problem is, that in method updateEating you change an attribute value (eating).
    CompundValue-classes (here Philosopher) do no allow this (they are immutable):
    You must create a brand new one with changed attribute value.

    Here is another idea how you could implement it.
    It uses TypeBinding instead of CompoundValue.

    The dining table is static - a sequence. The philosophers will sit here.
    The philosophers are instance based classes and all completely equal.
    Each has one fork (say left, your agent approach).
    Each can steal a fork from (say right) neighbour (i.e. NeighbourWithFork):

        public static class Room
        {
            public static Sequence<Philosopher> Table = new Sequence<Philosopher>();
            public static Philosopher GetNeighbourWithFork(Philosopher P)
            {
                return (null);
            }
        }
        public enum ForkState { free, grabbed, stolen };
        public enum AgentState { eating, talking };
        [TypeBinding("SpecExplorer1.Sample.ComplexThread")]
        public class Philosopher
        {
            ForkState Fork = ForkState.free;
            AgentState State = AgentState.talking;
            [Rule(Action = "new this.ComplexThread()")]
            Philosopher()
            {
                Room.Table = Room.Table.Add(this);
            }
            [Rule(Action = "this.Step()")]
            void GrabFork()
            {
            }
            [Rule(Action = "this.Step()")]
            void StealFork()
            {
            }
            [Rule(Action = "this.Step()")]
            void StopEating()
            {
            }
        }

    You can copy this and replace the original model code in the instance based example "SimpleThread.cs".
    You get this example, if you create a brand new instance based "SpecExplorer1"-project.

    Already now you can see how two philosophers take a seat at the table in the state browser,
    if you explore machine "SlicedThreadModelProgramm".

    What is left to do:
    * Implementing the rules, which change the state of the philosopher and his neighbour.
      Some examples:
      Grabing a fork is only allowed if fork is not stolen/already grabbed.
      Stealing is only possible if own fork is grabbed/neighbours fork is not already stolen.
      After stealing a fork the philosopher is eating.
    * Using a nice scenario which creates all five philosphers (here Threads from the example):
      machine FiveThreadScenario() : Main
      {
        new ComplexThread{5}; (_* |?| (!call new ComplexThread)*)
      }
    * Mapping the rules on own actions/class in the adapter (at the moment i.e. "ComplexThread.Step")

    Hope this helps.

     


    • Yanıt Olarak Öneren Yiming Cao 11 Nisan 2012 Çarşamba 21:33
    • Yanıt Olarak İşaretleyen Jameleddine 12 Nisan 2012 Perşembe 04:32
    11 Nisan 2012 Çarşamba 15:17
  • Yes, as bububa mentioned, inheriting from CompoundValue means that you declare the type to be "value type", which is mutable and cannot be updated after construction (like you cannot update value 100 in C# language).

    If you want to have reference value semantic, you'll need to use type-binding instead of CompoundValue.


    Thanks, Yiming

    11 Nisan 2012 Çarşamba 21:33
  • B.T.W : maybe a general lesson I've learned:
    Be tight with state variables: If I like reusing code - so should I reuse state information.
    Redundant state information is likely causing bugs.
    In Spec Explorer another symptom of it can be state explosion.

    So in the example a crack could even get rid of the static state variable "public static Sequence<Philosopher>" used above.
    Spec Explorer keeps track of the instances and provides internally an equivalent array.
    You can get all the instances (filling here a local variable) at any time you need it:
    public Philosopher[] Table = Microsoft.Modeling.Xrt.State.GetInstances<Philosopher>();

    Maybe the code can be improved even further ...

    • Düzenleyen bububa 13 Nisan 2012 Cuma 14:39
    13 Nisan 2012 Cuma 09:52
  • Thank you very much Bububa.

    I would like to have a static system with a predefined set of Forks and philosophers like:

       public enum Philosophers {Albert, Herbert, Fredrich, Sina, Juan};
       public enum Forks {F1, F2, F3, F4, F5 };

    And add attributes for the Philosopher class:

        Philosophers Name;
        Forks rightFork;
        Forks leftFork;
        Boolean eating = false;
        Boolean hungry = true | false;  // Is there a way to make this choice not deterministic when calling the constructor of Philosopher ?

    Instead of having "Room.Table = Room.Table.Add(this); ", I would like to have an initialization rule to add the philosophers statically like this:

    Table.Add(new Philosopher(Albert, F5, F1, false, false ));

    Table.Add(new Philosopher(Hubert, F5, F1, false, false ));

    etc.

    Next I need to model a function to check for fork ownership, ForkOwner: Forks ---> Philosophers.

    So far I was not successful in modeling it. Would you please help me achieve this ?

    Thanks.

    • Düzenleyen Jameleddine 15 Nisan 2012 Pazar 07:13 not finished editing
    15 Nisan 2012 Pazar 07:06
  • Hi Jamel,

    Switching to the static approach (AccumulatorModelProgram) this is another idea:

    	public enum Philosophers { Albert,Juan };
            public class Philosopher
            {
                public string Name;
                public bool hungry;
                public Philosopher(Philosophers P)
                {
                    this.Name = P.ToString();
                }
            }
            public class AccumulatorModelProgram
            {
                public static AccumulatorModelProgram I = new AccumulatorModelProgram();
                public static Map<Philosophers, Philosopher> Table;
                [Rule]
                public static void GrabFork(Philosophers P)
                {
                    Table[P].hungry = true;
                }
                public AccumulatorModelProgram()
                {
                    Table = new Map<Philosophers, Philosopher>();
                    Table = Table.Add(Philosophers.Albert, new Philosopher(Philosophers.Albert));
                    Table = Table.Add(Philosophers.Juan, new Philosopher(Philosophers.Juan));
                }
            }

    Adding to all configurations in cord:

    action abstract static void Accumulator.GrabFork(SpecExplorer1.Philosophers P);

    you can directly explore it again, if you replace the original model code.

    Some ideas:
    * I like to be tight with state variables : so only one state variable for each "Fork",
    but of course you can model two separate state variables for one fork.
    Spec Explorer will find possible pitfalls due to this anyway.
    * Maybe you want to have different initial conditions in the constructor (Juan eating or hungry etc.).
    This can be done by converting the constructor to a rule-method, which creates all initial conditions you are interested in.
    Of course if this rule is an event it can get the initial state from the SUT (non-determinism).

    Hope this helps.



    • Düzenleyen bububa 16 Nisan 2012 Pazartesi 10:12
    16 Nisan 2012 Pazartesi 10:11
  • Thank you very much Bububa for your help.

    In my code I have created a map (ForkOwner) to map forks to philisophers as follows:

                  

        public enum Philosophers { Albert, Herbert, Fredrich, Sina, Juan};    
        public enum Forks { F1, F2, F3, F4, F5 };
        
        public class Philosopher
        {
            public string Name;
            public Forks rightFork;
            public Forks leftFork;
            public bool hungry;
            public bool eating;

            public Philosopher(Philosophers P, Forks rf, Forks lf, bool eat)
            {
                this.Name = P.ToString();
                this.rightFork = rf;
                this.leftFork = lf;            
                this.eating = eat;
                this.hungry = true;
            }
        }
        public class AccumulatorModelProgram
        {
            public static AccumulatorModelProgram I = new AccumulatorModelProgram();
            public static Map<Philosophers, Philosopher> Table;
            public static Map<Forks, Philosophers> ForkOwner;
                  
            [Rule]
            public static void StartEating(Philosophers P)
            {
               Condition.IsTrue((Table[P].hungry) && (!Table[P].eating));         
               ForkOwner[Table[P].leftFork] = P;           
               ForkOwner[Table[P].rightFork] = P;
               Table[P].eating = true;
               
            }

            [Rule]
            public static void StopEating(Philosophers P)
            {
                Condition.IsTrue((!(Table[P].hungry) && Table[P].eating));
                //ForkOwner[Table[P].leftFork] = P;
                //ForkOwner[Table[P].rightFork] = P;            
                Table[P].eating = false;
            }

            public AccumulatorModelProgram()
            {
                Table = new Map<Philosophers, Philosopher>();            
                Table = Table.Add(Philosophers.Albert, new Philosopher(Philosophers.Albert, Forks.F5, Forks.F1, false));
                Table = Table.Add(Philosophers.Herbert, new Philosopher(Philosophers.Herbert, Forks.F1, Forks.F2, false));
                Table = Table.Add(Philosophers.Fredrich, new Philosopher(Philosophers.Fredrich, Forks.F2, Forks.F3, false));
                Table = Table.Add(Philosophers.Sina, new Philosopher(Philosophers.Sina, Forks.F3, Forks.F4, false));
                Table = Table.Add(Philosophers.Juan, new Philosopher(Philosophers.Juan, Forks.F4, Forks.F5, false));

                ForkOwner = new Map<Forks, Philosophers>();
                ForkOwner = ForkOwner.Add(Forks.F1, Philosophers.Albert);
                ForkOwner = ForkOwner.Add(Forks.F2, Philosophers.Albert);
                ForkOwner = ForkOwner.Add(Forks.F3, Philosophers.Albert);
                ForkOwner = ForkOwner.Add(Forks.F4, Philosophers.Albert);
                ForkOwner = ForkOwner.Add(Forks.F5, Philosophers.Albert);

            }
        }

    This code compiles fine but the exploration would generate an error state after S0, call error (). The description does not add much insight:

    Error    1    reached error state(s) (see graph/output window)    Spec Explorer    0    0    

    The issue is with the statement:        ForkOwner[Table[P].leftFork] = P;  

    Any idea about what is wrong with it ?

    Thanks

    Jamel.
    16 Nisan 2012 Pazartesi 20:06
  • Map is also a CompoundValue and thus immutable. If you click the error state on the exploration graph, you'll probably see an exception saying that map is read-only. You should use "Add" or "Override" API to get an updated copy of a map.


    Thanks, Yiming

    16 Nisan 2012 Pazartesi 20:25
  • Thanks Yiming.

    I have converted it to MapContainer and it looks working now.

    Thanks again.

    Jamel.

    17 Nisan 2012 Salı 02:44
  • Hi folks,

    Here is my updated code:

        public enum Philosophers { Albert, Herbert, Fredrich, Sina, Juan};    
        public enum Forks { F1, F2, F3, F4, F5 };   
        public class Philosopher
        {
            public string Name;
            public Forks rightFork;
            public Forks leftFork;
            public bool hungry;
            public bool eating;

            public Philosopher(Philosophers P, Forks rf, Forks lf, bool hun)
            {
                this.Name = P.ToString();
                this.rightFork = rf;
                this.leftFork = lf;            
                this.eating = false;
                this.hungry = hun;
            }       
        }
        public class AccumulatorModelProgram
        {
            public static AccumulatorModelProgram I = new AccumulatorModelProgram();
            public static Map<Philosophers, Philosopher> Table;
            public static MapContainer<Forks, Philosophers> ForkOwner;
            [Rule]
            public static void StartEating(Philosophers P)
            {
               Condition.IsTrue((Table[P].hungry) && (!Table[P].eating));
               Condition.IsTrue(!ForkOwner.ContainsKey(Table[P].leftFork) && !ForkOwner.ContainsKey(Table[P].rightFork));
     
               if (ForkOwner.ContainsKey(Table[P].leftFork) && ForkOwner.ContainsKey(Table[P].rightFork))
               {
                   ForkOwner[Table[P].leftFork] = P;
                   ForkOwner[Table[P].rightFork] = P;
               }
               else
               {
                   ForkOwner.Add(Table[P].leftFork, P);
                   ForkOwner.Add(Table[P].rightFork, P);
               }                      
                
               Table[P].eating = true;
               Table[P].hungry = Choice.Some<bool>();
            }

            [Rule]
            public static void StopEating(Philosophers P)
            {
                Condition.IsTrue((!Table[P].hungry) && (Table[P].eating));
                
                if (ForkOwner.ContainsKey(Table[P].leftFork) && ForkOwner.ContainsKey(Table[P].rightFork))
                {
                    ForkOwner.Remove(Table[P].leftFork);
                    ForkOwner.Remove(Table[P].rightFork);                  
                }                   
                Table[P].eating = false;
                Table[P].hungry = Choice.Some<bool>();
            }       
            public AccumulatorModelProgram()
            {
                Table = new Map<Philosophers, Philosopher>();
                Table = Table.Add(Philosophers.Albert, new Philosopher(Philosophers.Albert, Forks.F5, Forks.F1, true));
                Table = Table.Add(Philosophers.Herbert, new Philosopher(Philosophers.Herbert, Forks.F1, Forks.F2, false));
                Table = Table.Add(Philosophers.Fredrich, new Philosopher(Philosophers.Fredrich, Forks.F2, Forks.F3, false));
                Table = Table.Add(Philosophers.Sina, new Philosopher(Philosophers.Sina, Forks.F3, Forks.F4, false));
                Table = Table.Add(Philosophers.Juan, new Philosopher(Philosophers.Juan, Forks.F4, Forks.F5, false));
                ForkOwner = new MapContainer<Forks, Philosophers>();
                  }
        }

    I have a couple of questions:

    1) When I explore my system, I found loops with "call StartEating(Albert)" then "return StartEating", "call StopEating(Albert)" then "return StopEating".

    Is there a way to reduce the graph to the rule names without calls/returns ?

    2) I have tried to have a nondeterministic initialization of the hungry attribute in the constructor as follows:

    this.hungry = Choice.Some<bool>();

    This has generated an error. is there another way to achieve the same thing differently ?

    Thanks,

    Jamel.

    17 Nisan 2012 Salı 20:25
  • Hi Jamel,

    if you replace in cord for all your rule methods
    action abstract static void Accumulator.GrabFork(SpecExplorer1.Philosophers P);
    with
    action abstract event static void Accumulator.GrabFork(SpecExplorer1.Philosophers P);
    you remove the deterministic "call".    

    The idea is, that at the moment the rules ("StartEating", "StopEating") are not events.
    So they have a deterministic part ("call StartEating(...)" tranfering the argument
    and a non-deterministic part ("return StartEating).
    But all your rules use "Choice.Some". So they are indeed events.
    So they can simply end in different non-deterministic final states. They can't be merged.

    To your error: The problem I guess is, that already state S0 is not only one state, but
    a set of (non-deterministi)c states. This can't be executed against a real SUT. You have to convert the constructor to an event rule method (e.g."Init"), as I've mentioned in another posting above.

    Hope this helps

    18 Nisan 2012 Çarşamba 07:41
  • Thanks Bububa for your insights.

    I have kept the system as having one constructor to create the different objects that I need. However, I'm not using just one entry to the program (similar to the agent approach). Rule PhilosopherProgram will call StartEating and StopEating. Here I'm providing the complete code:


    public enum Philosophers {Albert, Herbert, Fredrich, Sina, Juan};    
    public enum Chopstick { c1, c2, c3, c4, c5 };
            
        public class Philosopher
        {
            public string Name;     
             public Philosopher(Philosophers P)
            {
                this.Name = P.ToString();            
            }
       }
        public class AccumulatorModelProgram
        {
            public static AccumulatorModelProgram I = new AccumulatorModelProgram();
            public static Map<Philosophers, Philosopher> Table;
            public static MapContainer<Philosophers, bool> Eating;
            public static MapContainer<Philosophers, bool> Hungry;
            public static MapContainer<Philosophers, Chopstick> leftChop;
            public static MapContainer<Philosophers, Chopstick> rightChop;
            public static MapContainer<Chopstick, Philosophers> ChopOwner;
               
            [Rule]
            public static void PhilosopherProgram(Philosophers P)
            {
                if ((Hungry[P]) && !Eating[P])
                    if (!ChopOwner.ContainsKey(leftChop[P]) && !ChopOwner.ContainsKey(rightChop[P]))
                        StartEating(P);
                    else
                       Console.WriteLine(P +" is hungry but can't eat !");
                 if (!Hungry[P] && Eating[P])
                     StopEating(P);

                Hungry[P] = !Hungry[P]; // Made it deterministic
            }
           
            public static void StartEating(Philosophers P)
            {            
               ChopOwner[leftChop[P]] = P;
               ChopOwner[rightChop[P]] = P;
               Eating[P] = true;
               Console.WriteLine(P + " starts eating.");
            }

            public static void StopEating(Philosophers P)
            {
                if (ChopOwner.ContainsKey(leftChop[P]) && ChopOwner.ContainsKey(rightChop[P]))
                {
                    ChopOwner.Remove(leftChop[P]);
                    ChopOwner.Remove(rightChop[P]);                  
                }
                Eating[P] = false;
                Console.WriteLine(P + " stops eating.");                     
            }
                     
            public AccumulatorModelProgram()
            {
                Table = new Map<Philosophers, Philosopher>();            

                Hungry = new MapContainer<Philosophers, bool>();
                Eating = new MapContainer<Philosophers, bool>();
                leftChop = new MapContainer<Philosophers, Chopstick>();
                rightChop = new MapContainer<Philosophers, Chopstick>();
                ChopOwner = new MapContainer<Chopstick, Philosophers>();

                foreach (Philosophers value in Enum.GetValues(typeof(Philosophers)))
                {
                    Table.Add(value, new Philosopher(value));
                    Eating.Add(value, false);              
                }        

                Hungry.Add(Philosophers.Albert, true);
                Hungry.Add(Philosophers.Herbert, false);
                Hungry.Add(Philosophers.Fredrich, false);
                Hungry.Add(Philosophers.Sina, false);
                Hungry.Add(Philosophers.Juan, false);
                
                // Initialize leftChop      
                leftChop.Add(Philosophers.Albert, Chopstick.c5);
                leftChop.Add(Philosophers.Herbert, Chopstick.c1);
                leftChop.Add(Philosophers.Fredrich, Chopstick.c2);
                leftChop.Add(Philosophers.Sina, Chopstick.c3);
                leftChop.Add(Philosophers.Juan, Chopstick.c4);

                // Initialize rightChop
                rightChop.Add(Philosophers.Albert, Chopstick.c1);
                rightChop.Add(Philosophers.Herbert, Chopstick.c2);
                rightChop.Add(Philosophers.Fredrich, Chopstick.c3);
                rightChop.Add(Philosophers.Sina, Chopstick.c4);
                rightChop.Add(Philosophers.Juan, Chopstick.c5);                                       
            }        
        }
    }

    The PhilosopherProgram is an event:
    action abstract event static void Accumulator.PhilosopherProgram(SpecExplorer2.Philosophers P);

    1) From the traces (debug output), I'm noticing a very strange behaviour. I'm starting with only Hungry[Albert]=true and nobody is eating. Rule PhilosopherProgram is executed ONCE for all the 5 philosophers with their corresponding mapcontainers Hungry and eating updated correctly. In this case, Albert will execute StartEating (eating[Albert] becomes true and Hungry[Albert] becomes false). All other philosophers will have Hungry[X] = true.

    Then when Rule PhilosopherProgram is called for the second time, I see that Eating[Albert] = false and Hungry[Albert]=true (which is the initial state). For me it is strange, Am I missing something here ? Please help.

    2) The exploration of the model would show only event PhilosopherProgram, which I believe, is expected since StartEating and StopEating are no longer declared as rules. Given the exploration graph, I cannot tell which method is invoked (other than looking at the debug output) ?

    3) Is there a way to keep StartEating and StopEating as rules and prevent their execution outside of the PhilosopherProgram ? This way I will see them in the exploration graph.

    4) I would like to derive test cases from my model. I believe that I should define an AcceptingStateCondition. As an example, I have tried the following:
    [AcceptingStateCondition]
            static bool Accept()
            {
                return (!Hungry[Philosophers.Albert]); //only states where Albert is not hungry are accepting
            }

    and this has resulted in:

    FATAL ERROR: Non-serializable exception:
    Message:Exception of type 'Microsoft.Z3.Z3Error' was thrown.
    Stack Trace:
       at Microsoft.Z3.get_ast(IntPtr t)
    ...

    Any idea what is wrong ?

    Thanks a lot for your help

    Jamel.
    • Düzenleyen Jameleddine 20 Nisan 2012 Cuma 10:56 provide more info
    20 Nisan 2012 Cuma 06:55
  • Hi Jamel,

    Your questions are good, don't know if my answers are:

    to 1) You are not printing from the test-adapter, but directly from the model. This has some risk.
    Can you replace your WriteLine with "Requirement.Capture("P +" is hungry but can't eat !");".
    With this you can see the output in the exploration, if you activate the requirements.

    to 2a)
    Yes, StartEating and StopEating must be rules, if you want to see them in the exploration.

    to 2b)
    You would prefer to see a reaction of rule "PhilosopherProgramm".
    So you like to split one rule-step "PhilosopherProgramm" into several rule-steps.
    I think this is always possible.
    You "only" have to find the right constraints for the sub-rules.

    to 2c)
    I guess 2b) is the fundamental reason why in your case "StartEating(P)" is not very natural as rule.
    Indeed StartEating is under constraint by indirect state variables. Finding the right constraints can be tough.
    I guess the natural input/output of your robots would be "GrabFork(...)" (and "ReleaseForks" identical to StopEating).
    If two forks are grabbed the robot is eating automatically.
    Rules should be preferably independent inputs/outputs.

    to 3)
    On the other hand this is a very common pattern we have very often.
    That is why we have a certain "modeling-library" with a member "StartCall" (e.g. "StartCall("StartEating")" in "PhilosopherProgramm").
    So we replace the direct call "StartEating(P)" with this.
    The result is, that in the exploration after step "PhilosopherProgramm", if and only if "StartCall("StartEating")" was executed
    we force to happen rule "StartEating(P)" as next step. In all other cases rule "StartEating(P)" is blocked.
    The arguments of the call are states (maybe for just one step).

    to 4)
    Have no clue have not tried your code so far.

    Hope this helps somehow.

    ============================

    Add-On:

    To 4) Unfortunately I was not able to reproduce the error.

    • Düzenleyen bububa 23 Nisan 2012 Pazartesi 08:03
    20 Nisan 2012 Cuma 16:35
  • Thanks Bububa.

    Would you please provide more info about StartCall method ? Is there a library that I should include or a cord config statement that I should include ?

    For now, as a work around, I'm protecting my call using a boolean expression (like a semaphore) and I place "Condition.IsTrue(StartEatingEnabled)" in the called rule.

    Thanks a lot for your help Bububa.

    Jamel.

    24 Nisan 2012 Salı 07:05
  • Hi Jamel,

    I think classifying the rule methods into
    SUT-stimulation (GrabFork, ReleaseFork)
    and SUT-responses (StartEating, StopEating - the rules which are
    enabled if a certain condition in the two stimulation rules is called before) is very powerful, but not fully general and unambigous.
    I think the definition depends on the domain - So it is not found in Microsoft.Modeling.
    (And probably you will define this already different to my understanding).

    I have written an own "modeling-lib" for "StartCall" for our domain, which also includes time.
    This implementation is exactly how you mentioned it, only a little bit generalized:
    Example: your variable "StartEatingEnabled" is an element of a map (called e.g. "Calls" with attribute "name" etc.).
    A map-element with name="StartEating" will be added by "StartCall("StartEating")".
    Rule "StartEating" is blocked with another method, which checks for this map-element.
    Sometimes you also want to block the stimulation rules if rule "StartEating" is enabled (GrabFork/ReleaseFork).

    Hope this helps

    24 Nisan 2012 Salı 09:56