By Design by contract, we mean add pre or post condition to our ecore model in order to add constraints on the Fsm's execution. It permits to use good practices into kermeta development. You can retrieve the Design by Contract concepts languages like Eiffel. Firstly, we present how to run configurations to parametrize this pre or post conditions. Then we present examples of pre and post conditions. In this section we study the example available in fr.irisa.kemeta.samples.fsm.demoAspect.
We want to execute an FSM model. To do that we must call the "run" operation of the "FSM" class. We are going to do that thanks to a KerMeta script. This script will : load an instance of the FSM meta model stored in a file and call the run operation of these instance.
![[Tip]](gfx/admonitions/tip.gif) | Tip |
|---|---|
To launch a script, the interpreter must know the entry point of the program. It can "ask" it to the user thanks to an Eclipse window. Another way might be to add the following statements into your kermeta code :
|
In the FSM example ( fr.irisa.triskell.kermeta.samples.fsm.demoAspect) , those scripts are in the "launcher" directory. Look at "minimization.kmt" script. Here the interpreter knows that entry point of the program is the operation "main" in the "Minimization" class.
Let's have a look at the file named "minimization.kmt". Open it. Look at the code of the main operation. There is no parameter. To run this script with constraint checking, right click on "minimization.kmt" and select "Run As" and "Kermeta Constrained Application". To run this script without constraint checking, right click on "minimization.kmt" and select "Run As" and "Run As Kermeta Application".
The program asks you for a filename. Put in "../models/sample1.fsm" for example. You are lastly asked for a filename which will correspond to the file generated by the program. Put in "../generated.fsm" and see the execution.
Now if you have a look at the three others scripts (checkInvariants, determinization and fsmLauncher) into fr.triskell.kermeta.samples.fsm.demoAspect/launcher you will notice that the main operation of the main class takes one argument. Let's focus on "fsmLauncher.kmt" launcher. The main operation takes one parameter which is the name of the file containing the FSM model. It loads the model, prints it and runs it. If you try the running method above, an exception is raised because the parameterized file does not exist. Indeed we did not specify any filename to the program. So, you cannot use the method above to run those kind of script. That is the reason why we are going to use run configurations. Then right click on "fsmLauncher.kmt" file and select "Run As" and "Run Configurations...". A window appears like the one below. Select the run configuration named "loaderFSM" and look at the different options. Have a special look at the file parameters :
"Location of your program file", here this is "fsmLauncher.kmt" filename relative to the project's root directory.
"Class qualified name", that is to say the main class of the program.
"Operation name", that is to say the main operation of the main class.
"Operation arguments", the parameters you want to send to the main operation.
Here, we give the string "../models/sample1.fsm" as a parameter to mainLoadFSM operation to "fsm::Main" class. By clicking on "Run" button, it will start the execution. You can create yourself some new run configurations. Just by left clicking on "Kermeta Application " or "Kermeta Constraint Application" (depending on the constraint checking you want) and select "New" and fill in the required fields.
![[Caution]](gfx/admonitions/caution.gif) | Caution |
|---|---|
Eclipse is slash sensible. It only accepts front slash and no backslash. Then /fr.irisa.triskell.kermeta.samples.fsm.demo/launcher/fsmLauncher.kmt is a valid filename whereas \fr.irisa.triskell.kermeta.samples.fsm.demo\launcher\fsmLauncher.kmt is not. |
| Tip |
|---|---|
If you want to create a new configuration, just right click on Kermeta Application, or Kermeta Constrained Application and New. Then, fill the fields like above. |
This section will present an example of constraint checking execution. Have a look at the "fsm.kmt" file (into fr.triskell.kermeta.samples.fsm.demo/kermeta. This kermeta file requires two files :
fsm_Operationnal_Semantics.kmt from fr.triskell.kermeta.samples.fsm.demo/kermeta/semantics/ which defines the fsm 's behaviour ( cf section Behaviour )
The following code shows the behaviour of the step operation :
aspect class State { reference combination : Set<State> // Go to the next state operation step(c : String) : String raises FSMException is do // Get the valid transitions var validTransitions : Collection<Transition> validTransitions := outgoingTransition.select { t | t.input.equals(c) } // Check if there is one and only one valid transition if validTransitions.empty then raise NoTransition.new end if validTransitions.size > 1 then raise NonDeterminism.new end // Fire the transition result := validTransitions.one.fire end // Create a new state from self state operation copy() : State is do result := State.new result.name := String.clone(name) result.combination := Set<State>.new end }Tip The key-word aspect (cf Behaviour ) permits to add some operations.
FSMConstraints.kmt from fr.triskell.kermeta.samples.fsm.demo/kermeta/constraints/ which defines an invariant and pre and post conditions.
aspect class State{ inv invariant1 is do self.outgoingTransition.forAll{ tr1 | self.outgoingTransition.forAll{ tr2 | tr2.input.equals(tr1.input).equals(tr1.equals(tr2))}} end } aspect class State{ operation step(c : String) :String pre pre2 is do c.equals(void).~not.~and(c.size.isGreater(0)) end post post3 is do result.equals(void).~not.~and(result.size.isGreater(0)) end is abstract }
There is a pre condition (pre2) which says that the character given as a parameter must not be void or empty string. The post condition (post3) says that the result must not be void or empty string. For each "step" method call, the pre and post conditions will be checked. If there are evaluated as false, the program is aborted otherwise the program goes on. Look at the run configuration named "FSM Aspect loader with pre-post check". If you do not retrieve this configuration right click on FSM Aspect loader with pre-post check.launch Run As -> FSM Aspect loader with pre-post check. Open the file (../models/sample1postv.fsm) used as parameter for this configuration. Observe the finite state diagram.
Execute "FSM Aspect loader with pre-post check" configuration. When you are asked for a letter , just press enter to send an empty string. Normally, it should provoke the violation of the pre condition. You should obtain the following trace into the console :
State : s1 Transition : s1-(c/NC)->s2 State : s2 Transition : s2-(x/y)->s2 Current state : s1 give me a letter : stepping... [kermeta::exceptions::ConstraintViolatedPre:4603] pre pre2 of operation step of class State violated
Execute "FSM Aspect loader with pre-post check" configuration. When you are asked for a letter , press c and then press enter. Normally, the post condition will be violated because the result will be an empty string. You should obtain the following trace into the console :
State : s1 Transition : s1-(c/NC)->s2 State : s2 Transition : s2-(x/y)->s2 Current state : s1 give me a letter : c c stepping... [kermeta::exceptions::ConstraintViolatedPost:5548] post post3 of operation step of class State violated
This chapter presented the use of pre and post condition on an execution.The next chapter explain how you can simulate an execution of the modelling system thank to behaviour.