locked
Handling Containers inside the model RRS feed

  • Question

  • I have a model, where i am making use of the MapContainer. Now the problem i am facing is that when i generate the model, it generates different states for the same functions based on the contents in the Container. Can't i limit it to check if (Container.Items.Count == X) then go to the same state, irrespective of the value of contents of the container?

     

    This is how my model code looks:

    using System;
    using System.Collections.Generic;
    using System.Text;
    
    using Microsoft.Modeling;
    
    namespace SpecExplorer9
    {
        public static class Model
        {
            public static MapContainer<int,int> numbers = new MapContainer<int,int>();
            public static int CurrentVal;
            /// <summary>
            /// An example model program.
            /// </summary>
            [Rule]
            static void AddNumber(int value)
            {
                CurrentVal++;
                numbers[CurrentVal] = value;
            }
    
            [Rule]
            static int ReadNumber(int value)
            {
                if (numbers.Keys.Contains(value))
                    return numbers[value];
                else
                    return 0;
            }
        }
    }
    
    

     

    and the cord file is

    

    // This is a Spec Explorer coordination script (Cord version 1.0).
    // Here you define configurations and machines describing the
    // exploration task you want to perform.
    
    /// Contains actions of the model, bounds, and switches.
    using SpecExplorer9;
    config Base 
    {
      action abstract static void SUT.AddNumber(int time);
      action abstract static int SUT.ReadNumber(int time);
    }
    
    config Product : Base
    {
      action abstract static void SUT.AddNumber(int time)
      where
      {.
        Condition.In(time, -1, 60, 3600);
      .};
    
      action abstract static int SUT.ReadNumber(int time)
      where
      {.
        Condition.In(time, -1, 60, 3600,4800);
      .};
    }
    // Action AddJob is synchronized, or matched, with the rule program using the
    // parameter values determined in the Product configuration.
    machine Product() : Product
    {
      AddNumber;ReadNumber || (construct model program from Product) 
    }
    
    

     

     

     

     

    Tuesday, November 15, 2011 1:38 PM

Answers

  • Hi Anirudh Goel - anigo,


    * A simple solution:
    Do not store different values in the state variable "numbers".
    Move this in the test-adapter. Unfortunately you have to do
    the check on the result in the test-adapter too. Your model is no oracle any more, becomes a simple "input generator", but all your combinations are still tested.


    * Only a "make-up"-solution - this will merge the states only visually:
     [Probe]
     public static int Count()
     {
        return (numbers.Count());
     }

     Add this to your model and add "Count" in the "Spec Explorer View Definition" as GroupQuery.

    * A more sophisticated solution would be to keep your method arguments symbolic:
    Unfortuantely your case is hitting exactly the two important points not working today:
    - State is built from a map, where elements would be symbolic
    - AND expansion needed after several transitions (posteriori).


    Hope this can help somehow.

    Wednesday, November 16, 2011 11:20 AM

All replies

  • Hi Anirudh Goel - anigo,


    * A simple solution:
    Do not store different values in the state variable "numbers".
    Move this in the test-adapter. Unfortunately you have to do
    the check on the result in the test-adapter too. Your model is no oracle any more, becomes a simple "input generator", but all your combinations are still tested.


    * Only a "make-up"-solution - this will merge the states only visually:
     [Probe]
     public static int Count()
     {
        return (numbers.Count());
     }

     Add this to your model and add "Count" in the "Spec Explorer View Definition" as GroupQuery.

    * A more sophisticated solution would be to keep your method arguments symbolic:
    Unfortuantely your case is hitting exactly the two important points not working today:
    - State is built from a map, where elements would be symbolic
    - AND expansion needed after several transitions (posteriori).


    Hope this can help somehow.

    Wednesday, November 16, 2011 11:20 AM
  • thanks bububa, i remodelled my scenario to be container less and as suggested ported it to the adapter.

    Thanks,

    Anirudh

    Wednesday, November 23, 2011 7:51 PM
  • Hi, Anirudh,

    I have marked bubuda's thread as answer.

    I also want to mention that many customer requested to "isolate" some parts of state variables, and only considers the rest parts in exploration. However, it will result in logic error. Imagine a case that you just care about the number of elements in MapContainer, but you still can write a rule like:

    [Rule]

    static void A()

    {

        Condition.IsTrue(numbers.Contains(5);

    }

    In this case, if all steps go to one state only caring about the number of elements, how do they split again when you have constraints related to the content?

    That is why there is no feature related to "state isolation"

    Thanks,

    Xiang

    Friday, November 25, 2011 9:38 AM
    Moderator