ARRANGE language

Files written in ARRANGE (*.arr) help you in arranging models, configurations, scenarios and test suites.

referenced SPIN PROMELA models

example

pml PmlFile { 
	import ".\datadriven2.pml" ;  
} 

referenced mCRL2 models

example

mcrl2 model1 {
	import ".\datadriven1.mcrl2" ; 
}  

scenarios (scenarios)

Container to construct FSM behaviours over

• proctypes,
• LTLs and
• labels. The FSMs operate over a set of labels which is specified via [labelref]. For definition of scenarios, express the construction of a Finite State Machine - from expressions over labels and composition of other express FSMs.

labels

Container to define a set of labels.

example

labels actionSet1symbolic {	
	out label_tx 	= "ch_tx!val1";
	out label_rx 	= "ch_rx?val1"; 
}  

notrace

example

notrace notrace1 {
	foo1_in!true,3;	
}

test

example

test t1 {
	configref cfg_main_depthFirst;
	notraceref notrace1;
}

testset

example

testset suite1_manualConstructs {
	testsuitedir = "..\..\msvs\datadriven1_tests";
	testref t1;	
}

config

Entries with prefix test. concern the c++ test generators. Entries with prefix verification. concern the SPIN model checker.

example

config cfg_main_depthFirst {
	test.adapter = machine1;
	test.harnessOutputQueue  = machine1MethodCalls;
	test.harnessOutputQueue = foo1_in;
	test.harnessInputQueue  = foo1_out;
	test.harnessOutputQueue = foo2_in;
	test.harnessInputQueue = foo2_out; 
	test.cppDir = "..\..\msvs\datadriven1_tests";
	test.cppSharedDir = "..\..\msvs\datadriven1_shared";
	test.cppNamespace  = "functionModeling3and4_tests";
	verification.safety.invalidEndstates = false; // gets disabled by never claim(s) anyways
	verification.safety.assertionViolations = true; // needed for verification of LTLs
	verification.safety.xrxsAssertions = false;
	verification.storageMode.bitstateSupertrace;
	verification.searchmode.depthFirst.partialOrderReduction = true; 
	verification.searchmode.depthFirst.boundedContextSwitching.withBound = 0; 
	verification.searchmode.reportUnreachableCode = true; 
	verification.fullChannels.blockNewMessages   ; 
	verification.advancedParameters.maxSearchDepthSteps  = 10000; /*10000 is default*/
	verification.advancedParameters.physMemAvailable = 1024;
}