Check all the invariants for a model can be useful if you use a model provided by a third party or resulting from a transformation, it permits to check well-formed rules. For more informations about it, please refer to the Model Checking Manual. Look at the file checkInvariants.kmt in fr.irisa.triskell.kermeta.samples.fsm.demoAspect/launcher/checkInvariants.kmt . This class permits to check all the invariants from the meta model thanks to the method checkAllInvariants.

    class InvariantChecker
    {
    operation main(input_automaton : String) : Void is do 
    var rep : EMFRepository init EMFRepository.new
    var theFSM : FSM init AutomatonHelper.new.loadEMFAutomaton(rep, input_automaton, "http://www.kermeta.org/fsm")
    
    // To check all contained elements by "theFSM"
    stdio.writeln("> call of the checkAllInvariants method")
    theFSM.checkAllInvariants
    // To check only the states that are contained in "theFSM"
    stdio.writeln("> call of the checkInvariants method")
    end
    }
    

Look at the Run Configuration FSM check invariant. If you run it you should obtain the following trace :

Figure 6.1. Fsm_scratch_sample view

Now, we will study the case of an error which violate an invariant. Look at the file FSMConstraints.kmt into fr.triskell.kermeta.fsm.demo/kermeta/constraints/FSMConstraints.kmt . You will see the following invariant

 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 } 

It means that several outgoing transitions from a state cannot have the same input. Look at the file samplerunErrorInvariant.fsm. Right click on Aspect check invariantsError and click on Apply and Run. This fsm model have two transitions with the same input. Like invariant is violated, Kermeta raises an exception. So, you should obtain the following trace :

Figure 6.2. Invariant error 's trace

Now you know how to check models. The next section explains how you can improve kermeta programs adding on them Design by contract which consist in adding pre and post conditions.