Add test related to model2K2.

Change-Id: I8720e55c08fb7d734ac872180eaede0b5afb90a4

plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/KratosFiles/MonitorPresence.k2

+(type State (enum primary ))
+(type InitTransition (enum init_to_pr ))
+(type Transition (enum pr_to_pr ))
+
+(entry main)
+
+(globals
+	; state machine variables
+	(var state State)
+	(var init_transition InitTransition)
+	(var transition Transition)
+	; input ports
+	(var input_is_present bool)
+	(var enabled bool)
+	; output ports
+	(var absence_alarm bool)
+	; attributes
+	; array length
+	
+	)
+
+(function init () (return)
+	(locals (var guard_cond bool))
+	(seq
+		(jump (label choice_init_trans_init_to_pr))
+		
+		; check if the current init transition is 'init_to_pr' 	
+		(label choice_init_trans_init_to_pr)
+			(call (const guard_init_to_pr (fun () (bool))) guard_cond)
+			(assume guard_cond)
+			(call (const effect_init_to_pr (fun () ())))
+			; update state machine variables
+			(assign state (const primary State))
+			(assign init_transition  (const init_to_pr InitTransition))
+		(jump (label end_init))
+		
+		(label end_init))
+)
+
+(function step () (return)
+	; the variable 'guard_cond' stores the value of each guard condition
+	(locals (var guard_cond bool))
+	(seq
+	    (jump (label choice_state_primary) )
+
+		; check if the current state is 'primary'
+		(label choice_state_primary)
+		(assume (op eq state (const primary State)))
+		(seq
+			(jump (label choice_trans_pr_to_pr)))
+		(jump (label end_step))
+		
+		; check if the current transition is 'pr_to_pr' 	
+		(label choice_trans_pr_to_pr)
+			(call (const guard_pr_to_pr (fun () (bool)))guard_cond)
+			(assume guard_cond)
+			(call (const effect_pr_to_pr (fun () ())))
+			; update state machine variables
+			(assign state (const primary State))
+			(assign transition (const pr_to_pr Transition))
+		(jump (label end_step))
+
+		
+		(label end_step))
+)
+
+; the RHS of the assignment of each function 'guard_...' is translated from the guards expressions written in CleanC
+(function guard_init_to_pr () (return (var ret bool))
+	(locals )
+	(seq
+		(assign ret (const |true| bool))
+		)
+	)
+	
+(function guard_pr_to_pr () (return (var ret bool))
+	(locals )
+	(seq
+		(assign ret (const |true| bool))
+		)
+	)
+	
+
+; the body of each function 'effect_...' is translated from the effects statements written in CleanC
+(function effect_init_to_pr () (return )
+	(locals )
+	(seq
+		(assign absence_alarm (const |false| bool))
+		)
+
+	)
+	
+(function effect_pr_to_pr () (return )
+	(locals (var |AndLogicOPImpl_0_res| bool) (var |NotLogicOPImpl_0_res| bool) (var |EqualImpl_0_res| bool) )
+	(seq
+		(assign NotLogicOPImpl_0_res (op not input_is_present))
+		(assign EqualImpl_0_res (op eq enabled (const |true| bool)))
+		(assign AndLogicOPImpl_0_res (op and NotLogicOPImpl_0_res EqualImpl_0_res))
+		(assign absence_alarm AndLogicOPImpl_0_res)
+		)
+
+	)
+
+(function read_inputs () (return)
+   (locals )
+   ;;(assume (const true bool))
+   (seq       
+	   ; input ports
+       (havoc input_is_present)
+       (havoc enabled)
+	   ; output ports
+	   (havoc absence_alarm)
+	   ; attributes
+     )
+   )
+   
+; the main function	
+(function main () (return)
+        (locals )
+        (seq
+           (call (const read_inputs (fun () ())))
+           (call (const init (fun () ())) )
+           (label LTL.init)
+           (call (const read_inputs (fun () ())))
+           (label while-true)
+           (label LTL.pre_step)
+           (call (const step (fun () ())) )
+           (call (const read_inputs (fun () ())))
+           (label LTL.post_step)
+           (jump (label while-true))
+           ))

plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/KratosFiles/Selector.k2

+(type State (enum input_1 input_2 ))
+(type InitTransition (enum init_to_in1 ))
+(type Transition (enum in1_to_in1 in1_to_in2 in2_to_in1 in2_to_in2 ))
+
+(entry main)
+
+(globals
+	; state machine variables
+	(var state State)
+	(var init_transition InitTransition)
+	(var transition Transition)
+	; input ports
+	(var input1 real)
+	(var input1_is_present bool)
+	(var input2 real)
+	(var input2_is_present bool)
+	(var switch_current_use bool)
+	; output ports
+	(var current_use int)
+	(var output real)
+	(var output_is_present bool)
+	; attributes
+	; array length
+	
+	)
+
+(function init () (return)
+	(locals (var guard_cond bool))
+	(seq
+		(jump (label choice_init_trans_init_to_in1))
+		
+		; check if the current init transition is 'init_to_in1' 	
+		(label choice_init_trans_init_to_in1)
+			(call (const guard_init_to_in1 (fun () (bool))) guard_cond)
+			(assume guard_cond)
+			(call (const effect_init_to_in1 (fun () ())))
+			; update state machine variables
+			(assign state (const input_1 State))
+			(assign init_transition  (const init_to_in1 InitTransition))
+		(jump (label end_init))
+		
+		(label end_init))
+)
+
+(function step () (return)
+	; the variable 'guard_cond' stores the value of each guard condition
+	(locals (var guard_cond bool))
+	(seq
+	    (jump (label choice_state_input_1) (label choice_state_input_2) )
+
+		; check if the current state is 'input_1'
+		(label choice_state_input_1)
+		(assume (op eq state (const input_1 State)))
+		(seq
+			(jump (label choice_trans_in1_to_in1)(label choice_trans_in1_to_in2)))
+		(jump (label end_step))
+		
+		; check if the current state is 'input_2'
+		(label choice_state_input_2)
+		(assume (op eq state (const input_2 State)))
+		(seq
+			(jump (label choice_trans_in2_to_in1)(label choice_trans_in2_to_in2)))
+		(jump (label end_step))
+		
+		; check if the current transition is 'in1_to_in1' 	
+		(label choice_trans_in1_to_in1)
+			(call (const guard_in1_to_in1 (fun () (bool)))guard_cond)
+			(assume guard_cond)
+			(call (const effect_in1_to_in1 (fun () ())))
+			; update state machine variables
+			(assign state (const input_1 State))
+			(assign transition (const in1_to_in1 Transition))
+		(jump (label end_step))
+
+		; check if the current transition is 'in1_to_in2' 	
+		(label choice_trans_in1_to_in2)
+			(call (const guard_in1_to_in2 (fun () (bool)))guard_cond)
+			(assume guard_cond)
+			(call (const effect_in1_to_in2 (fun () ())))
+			; update state machine variables
+			(assign state (const input_2 State))
+			(assign transition (const in1_to_in2 Transition))
+		(jump (label end_step))
+
+		; check if the current transition is 'in2_to_in1' 	
+		(label choice_trans_in2_to_in1)
+			(call (const guard_in2_to_in1 (fun () (bool)))guard_cond)
+			(assume guard_cond)
+			(call (const effect_in2_to_in1 (fun () ())))
+			; update state machine variables
+			(assign state (const input_1 State))
+			(assign transition (const in2_to_in1 Transition))
+		(jump (label end_step))
+
+		; check if the current transition is 'in2_to_in2' 	
+		(label choice_trans_in2_to_in2)
+			(call (const guard_in2_to_in2 (fun () (bool)))guard_cond)
+			(assume guard_cond)
+			(call (const effect_in2_to_in2 (fun () ())))
+			; update state machine variables
+			(assign state (const input_2 State))
+			(assign transition (const in2_to_in2 Transition))
+		(jump (label end_step))
+
+		
+		(label end_step))
+)
+
+; the RHS of the assignment of each function 'guard_...' is translated from the guards expressions written in CleanC
+(function guard_init_to_in1 () (return (var ret bool))
+	(locals )
+	(seq
+		(assign ret (const |true| bool))
+		)
+	)
+	
+(function guard_in1_to_in1 () (return (var ret bool))
+	(locals (var |NotLogicOPImpl_0_res| bool) )
+	(seq
+		(assign NotLogicOPImpl_0_res (op not switch_current_use))
+		(assign ret NotLogicOPImpl_0_res)
+		)
+	)
+	
+(function guard_in1_to_in2 () (return (var ret bool))
+	(locals (var |EqualImpl_0_res| bool) )
+	(seq
+		(assign EqualImpl_0_res (op eq switch_current_use (const |true| bool)))
+		(assign ret EqualImpl_0_res)
+		)
+	)
+	
+(function guard_in2_to_in1 () (return (var ret bool))
+	(locals (var |EqualImpl_0_res| bool) )
+	(seq
+		(assign EqualImpl_0_res (op eq switch_current_use (const |true| bool)))
+		(assign ret EqualImpl_0_res)
+		)
+	)
+	
+(function guard_in2_to_in2 () (return (var ret bool))
+	(locals (var |NotLogicOPImpl_0_res| bool) )
+	(seq
+		(assign NotLogicOPImpl_0_res (op not switch_current_use))
+		(assign ret NotLogicOPImpl_0_res)
+		)
+	)
+	
+
+; the body of each function 'effect_...' is translated from the effects statements written in CleanC
+(function effect_init_to_in1 () (return )
+	(locals )
+	(seq
+		(assign current_use (const |1| int))
+		(assign output (const |0.0| real))
+		(assign output_is_present (const |true| bool))
+		)
+
+	)
+	
+(function effect_in1_to_in1 () (return )
+	(locals )
+	(seq
+		(assign output input1)
+		(assign output_is_present input1_is_present)
+		)
+
+	)
+(function effect_in1_to_in2 () (return )
+	(locals )
+	(seq
+		(assign current_use (const |2| int))
+		(assign output input2)
+		(assign output_is_present input2_is_present)
+		)
+
+	)
+(function effect_in2_to_in1 () (return )
+	(locals )
+	(seq
+		(assign current_use (const |1| int))
+		(assign output input1)
+		(assign output_is_present input1_is_present)
+		)
+
+	)
+(function effect_in2_to_in2 () (return )
+	(locals )
+	(seq
+		(assign output input2)
+		(assign output_is_present input2_is_present)
+		)
+
+	)
+
+(function read_inputs () (return)
+   (locals )
+   ;;(assume (const true bool))
+   (seq       
+	   ; input ports
+       (havoc input1)
+       (havoc input1_is_present)
+       (havoc input2)
+       (havoc input2_is_present)
+       (havoc switch_current_use)
+	   ; output ports
+	   (havoc current_use)
+	   (havoc output)
+	   (havoc output_is_present)
+	   ; attributes
+     )
+   )
+   
+; the main function	
+(function main () (return)
+        (locals )
+        (seq
+           (call (const read_inputs (fun () ())))
+           (call (const init (fun () ())) )
+           (label LTL.init)
+           (call (const read_inputs (fun () ())))
+           (label while-true)
+           (label LTL.pre_step)
+           (call (const step (fun () ())) )
+           (call (const read_inputs (fun () ())))
+           (label LTL.post_step)
+           (jump (label while-true))
+           ))

plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/SSR_fi/KratosFiles/SpeedSensor.k2

+(type State (enum primary ))
+(type InitTransition (enum init_to_primary ))
+(type Transition (enum pr_to_pr ))
+
+(entry main)
+
+(globals
+	; state machine variables
+	(var state State)
+	(var init_transition InitTransition)
+	(var transition Transition)
+	; input ports
+	(var speed real)
+	; output ports
+	(var sensed_speed real)
+	(var sensed_speed_is_present bool)
+	; attributes
+	; array length
+	
+	)
+
+(function init () (return)
+	(locals (var guard_cond bool))
+	(seq
+		(jump (label choice_init_trans_init_to_primary))
+		
+		; check if the current init transition is 'init_to_primary' 	
+		(label choice_init_trans_init_to_primary)
+			(call (const guard_init_to_primary (fun () (bool))) guard_cond)
+			(assume guard_cond)
+			(call (const effect_init_to_primary (fun () ())))
+			; update state machine variables
+			(assign state (const primary State))
+			(assign init_transition  (const init_to_primary InitTransition))
+		(jump (label end_init))
+		
+		(label end_init))
+)
+
+(function step () (return)
+	; the variable 'guard_cond' stores the value of each guard condition
+	(locals (var guard_cond bool))
+	(seq
+	    (jump (label choice_state_primary) )
+
+		; check if the current state is 'primary'
+		(label choice_state_primary)
+		(assume (op eq state (const primary State)))
+		(seq
+			(jump (label choice_trans_pr_to_pr)))
+		(jump (label end_step))
+		
+		; check if the current transition is 'pr_to_pr' 	
+		(label choice_trans_pr_to_pr)
+			(call (const guard_pr_to_pr (fun () (bool)))guard_cond)
+			(assume guard_cond)
+			(call (const effect_pr_to_pr (fun () ())))
+			; update state machine variables
+			(assign state (const primary State))
+			(assign transition (const pr_to_pr Transition))
+		(jump (label end_step))
+
+		
+		(label end_step))
+)
+
+; the RHS of the assignment of each function 'guard_...' is translated from the guards expressions written in CleanC
+(function guard_init_to_primary () (return (var ret bool))
+	(locals )
+	(seq
+		(assign ret (const |true| bool))
+		)
+	)
+	
+(function guard_pr_to_pr () (return (var ret bool))
+	(locals )
+	(seq
+		(assign ret (const |true| bool))
+		)
+	)
+	
+
+; the body of each function 'effect_...' is translated from the effects statements written in CleanC
+(function effect_init_to_primary () (return )
+	(locals )
+	(seq
+		(assign sensed_speed (const |0| int))
+		(assign sensed_speed_is_present (const |true| bool))
+		)
+
+	)
+	
+(function effect_pr_to_pr () (return )
+	(locals )
+	(seq
+		(assign sensed_speed_is_present (const |true| bool))
+		(assign sensed_speed speed)
+		)
+
+	)
+
+(function read_inputs () (return)
+   (locals )
+   ;;(assume (const true bool))
+   (seq       
+	   ; input ports
+       (havoc speed)
+	   ; output ports
+	   (havoc sensed_speed)
+	   (havoc sensed_speed_is_present)
+	   ; attributes
+     )
+   )
+   
+; the main function	
+(function main () (return)
+        (locals )
+        (seq
+           (call (const read_inputs (fun () ())))
+           (call (const init (fun () ())) )
+           (label LTL.init)
+           (call (const read_inputs (fun () ())))
+           (label while-true)
+           (label LTL.pre_step)
+           (call (const step (fun () ())) )
+           (call (const read_inputs (fun () ())))
+           (label LTL.post_step)
+           (jump (label while-true))
+           ))

plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/src/org/polarsys/chess/contracts/verificationService/test/runtime/tests/TestBasicOperationsHeadless.java

@@ -19,6 +19,7 @@ import org.eclipse.papyrus.junit.utils.rules.ModelSetFixture;
 import org.eclipse.papyrus.junit.utils.rules.PluginResource;
 import org.eclipse.papyrus.junit.utils.rules.ResourceSetFixture;
 import org.eclipse.uml2.uml.Class;
+import org.eclipse.uml2.uml.Element;
 import org.eclipse.uml2.uml.Model;
 import org.eclipse.uml2.uml.Package;
 import org.junit.Before;
@@ -32,6 +33,7 @@ import org.polarsys.chess.service.core.model.ChessSystemModel;
 import org.polarsys.chess.service.core.model.UMLStateMachineModel;
 
 import eu.fbk.eclipse.standardtools.ModelTranslatorToOcra.core.services.OSSTranslatorServiceAPI;
+import eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv.core.services.K2TranslatorServiceAPI;
 import eu.fbk.eclipse.standardtools.StateMachineTranslatorToSmv.core.services.SMVTranslatorServiceAPI;
 import eu.fbk.tools.adapter.ui.preferences.PreferenceConstants;
 
@@ -154,6 +156,28 @@ public class TestBasicOperationsHeadless extends AbstractPapyrusTest {
 		String oracleFolder = projectFolderPath + "/SmvFiles";
 		TestResultsUtil.dirsAreEqual(oracleFolder, selectedDirectory, collector);
 	}
+	
+	@Test
+	@PluginResource(projectPath)
+	//@Ignore
+	public void testExportBlocksAsK2() throws Exception {
+		Model model = getModel();
+		
+		K2TranslatorServiceAPI k2TranslatorService = K2TranslatorServiceAPI
+				.getInstance(ChessSystemModel.getInstance(), UMLStateMachineModel.getInstance());
+
+		String selectedDirectory = testOutput;//"testOutput";
+		
+		Set<?> stateMachines = entityUtil.getNominalStateMachines(model);
+		logger.debug("stateMachines.size: " + stateMachines.size());
+		for (Object stateMachine : stateMachines) {
+			Class blockAsClass = (Class) entityUtil.getOwner((Element) stateMachine);
+			k2TranslatorService.exportBlockToK2File(blockAsClass, selectedDirectory, blockAsClass.getName(), null, new NullProgressMonitor());
+		}
+
+		String oracleFolder = projectFolderPath + "/KratosFiles";
+		TestResultsUtil.dirsAreEqual(oracleFolder, selectedDirectory, collector);
+	}
 
 	@Before
 	public void setTestParameters() throws Exception {