Merge remote-tracking branch 'origin/master' into menu_games

9 years ago · 12a25158b6
23 changed files with 866 additions and 86 deletions
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@ -354,10 +354,14 @@ set(STORM_GENERATED_SOURCES "${PROJECT_BINARY_DIR}/src/storm/utility/storm-versi
 include_directories("${PROJECT_BINARY_DIR}/include")

 include(CTest)
+# Compiles all tests
+add_custom_target(tests)
+# Compiles and runs all tests
 add_custom_target(check COMMAND ${CMAKE_CTEST_COMMAND})
 set(CMAKE_CTEST_COMMAND_VERBOSE ${CMAKE_CTEST_COMMAND} -V)
 add_custom_target(check-verbose COMMAND ${CMAKE_CTEST_COMMAND_VERBOSE})
-
+add_dependencies(check tests)
+add_dependencies(check-verbose tests)

 set(STORM_TARGETS "")
 add_subdirectory(src)
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@ -276,9 +276,8 @@ if(USE_HYPRO)
 	find_package(hypro QUIET REQUIRED)
 	if(hypro_FOUND)
 		set(STORM_HAVE_HYPRO ON)
-		message(STATUS "Storm - Linking with hypro ${hypro_VERSION_STRING}.")
+		message(STATUS "Storm - Linking with hypro.")
 		include_directories("${hypro_INCLUDE_DIR}")
-		link_directories( /Users/tim/hypro/build )
 		list(APPEND STORM_LINK_LIBRARIES ${hypro_LIBRARIES})
 	else()
 		message(FATAL_ERROR "StoRM - HyPro was requested but not found")
@ -364,14 +363,14 @@ add_imported_library(sylvan STATIC ${Sylvan_LIBRARY} ${Sylvan_INCLUDE_DIR})
 add_dependencies(sylvan_STATIC sylvan)
 list(APPEND STORM_DEP_TARGETS sylvan_STATIC)

-if(${OPERATING_SYSTEM} MATCHES "Linux")
-    find_package(Hwloc QUIET REQUIRED)
-    if(HWLOC_FOUND)
-        message(STATUS "Storm - Linking with hwloc ${HWLOC_VERSION}.")
-        add_imported_library(hwloc STATIC ${HWLOC_LIBRARIES} "")
-        list(APPEND STORM_DEP_TARGETS hwloc_STATIC)
-    else()
-        message(FATAL_ERROR "HWLOC is required but was not found.")
+find_package(Hwloc QUIET REQUIRED)
+if(HWLOC_FOUND)
+    message(STATUS "Storm - Linking with hwloc ${HWLOC_VERSION}.")
+    add_imported_library(hwloc STATIC ${HWLOC_LIBRARIES} "")
+    list(APPEND STORM_DEP_TARGETS hwloc_STATIC)
+else()
+    if(${OPERATING_SYSTEM} MATCHES "Linux")
+        message(FATAL_ERROR "HWLOC is required on Linux but was not found.")
    endif()
 endif()

--- a/resources/cmake/find_modules/FindHwloc.cmake
+++ b/resources/cmake/find_modules/FindHwloc.cmake
@ -19,7 +19,6 @@ if (NOT HWLOC_PREFIX AND NOT $ENV{HWLOC_BASE} STREQUAL "")
  set(HWLOC_PREFIX $ENV{HWLOC_BASE})
 endif()

-message(STATUS "Searching for hwloc library in path " ${HWLOC_PREFIX})

 find_library(
  HWLOC_LIBRARIES
@ -50,6 +49,4 @@ if (HWLOC_FOUND)
  if (NOT $ENV{HWLOC_LIB} STREQUAL "")
 # set(HWLOC_LIBRARIES "$ENV{HWLOC_LIB}")
  endif()
-  message(STATUS "hwloc includes:  " ${HWLOC_INCLUDE_DIRS})
-  message(STATUS "hwloc libraries: " ${HWLOC_LIBRARIES})
 endif()
--- a/resources/examples/testfiles/ma/server.ma
+++ b/resources/examples/testfiles/ma/server.ma
@ -0,0 +1,34 @@
+
+ma
+
+const double rateProcessing = 2;
+const double rateA = 1;
+const double rateB = 1;
+
+module server
+	
+	s : [0..5]; // current state:
+	// 0: wait for request	
+	// 1: received request from A
+	// 2: received request from B	
+	// 3: starting to process request of B
+	// 4: processing request
+	// 5: error
+	
+	
+	
+	<> s=0 -> rateA : (s'=1) + rateB : (s'=2);
+	[alpha] s=1 -> 1 : (s'=4);
+	[alpha] s=2 -> 1 : (s'=3);
+	[beta]  s=2 -> 0.5 : (s'=0) + 0.5 : (s'=3);
+	[] s=3 -> 1 : (s'=4);
+	<> s=4 -> rateProcessing : (s'=0) + (rateA+rateB) : (s'=5);
+	<> s=5 -> 1 : true;
+	
+endmodule
+
+
+label "error" = (s=5);
+label "processB" = (s=3);
+
+
--- a/resources/examples/testfiles/mdp/multiobj_consensus2_3_2.nm
+++ b/resources/examples/testfiles/mdp/multiobj_consensus2_3_2.nm
@ -0,0 +1,88 @@
+// model of randomised consensus
+
+mdp
+
+const int N = 2; // num processes
+const int MAX = 3; // num rounds (R)
+const int K = 2; // Parameter for coins
+
+// need to turn these into local copies later so the reading phase is complete?
+formula leaders_agree1 = (p1=1 | r1<max(r1,r2)) & (p2=1 | r2<max(r1,r2));
+formula leaders_agree2 = (p1=2 | r1<max(r1,r2)) & (p2=2 | r2<max(r1,r2));
+
+formula decide1 = leaders_agree1 & (p1=1 | r1<max(r1,r2)-1) & (p2=1 | r2<max(r1,r2)-1);
+formula decide2 = leaders_agree2 & (p1=2 | r1<max(r1,r2)-1) & (p2=2 | r2<max(r1,r2)-1);
+
+module process1
+
+	s1 : [0..5]; // local state
+	// 0 initialise/read registers
+	// 1 finish reading registers (make a decision)
+	// 1 warn of change
+	// 2 enter shared coin protocol
+	// 4 finished
+	// 5 error (reached max round and cannot decide)
+	r1 : [0..MAX]; // round of the process
+	p1 : [0..2]; // preference (0 corresponds to null)
+
+	// nondeterministic choice as to initial preference
+	[] s1=0 & r1=0 -> (p1'=1) & (r1'=1);
+	[] s1=0 & r1=0 -> (p1'=2) & (r1'=1);
+	
+	// read registers (currently does nothing because read vs from other processes
+	[] s1=0 & r1>0 & r1<=MAX -> (s1'=1);
+	// maxke a decision
+	[] s1=1 & decide1 -> (s1'=4) & (p1'=1);
+	[] s1=1 & decide2 -> (s1'=4) & (p1'=2);
+	[] s1=1 & r1<MAX & leaders_agree1 & !decide1 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
+	[] s1=1 & r1<MAX & leaders_agree2 & !decide2 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
+	[] s1=1 & r1<MAX & !(leaders_agree1 | leaders_agree2) -> (s1'=2) & (p1'=0);
+	[] s1=1 & r1=MAX & !(decide1 | decide2) -> (s1'=5); // run out of rounds so error
+	// enter the coin procotol for the current round
+	[coin1_s1_start] s1=2 & r1=1 -> (s1'=3);
+	[coin2_s1_start] s1=2 & r1=2 -> (s1'=3);
+	// get response from the coin protocol
+	[coin1_s1_p1] s1=3 & r1=1 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
+	[coin1_s1_p2] s1=3 & r1=1 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
+	[coin2_s1_p1] s1=3 & r1=2 -> (s1'=0) & (p1'=1) & (r1'=r1+1);
+	[coin2_s1_p2] s1=3 & r1=2 -> (s1'=0) & (p1'=2) & (r1'=r1+1);
+	// done so loop
+	[done] s1>=4 -> true; 
+
+endmodule
+
+module process2 = process1[ s1=s2,
+											p1=p2,p2=p1,
+											r1=r2,r2=r1,
+											coin1_s1_start=coin1_s2_start,coin2_s1_start=coin2_s2_start,
+											coin1_s1_p1=coin1_s2_p1,coin2_s1_p1=coin2_s2_p1,
+											coin1_s1_p2=coin1_s2_p2,coin2_s1_p2=coin2_s2_p2 ]
+endmodule
+
+module coin1_error
+	
+	c1 : [0..1]; // 1 is the error state
+	v1 : [0..2]; // value of the coin returned the first time
+	
+	// first returned value (any processes)
+	[coin1_s1_p1] v1=0 -> (v1'=1);
+	[coin1_s2_p1] v1=0 -> (v1'=1);
+	[coin1_s1_p2] v1=0 -> (v1'=2);
+	[coin1_s2_p2] v1=0 -> (v1'=2);
+	// later values returned
+	[coin1_s1_p1] v1=1 -> true; // good behaviour
+	[coin1_s2_p1] v1=1 -> true; // good behaviour
+	[coin1_s1_p2] v1=2 -> true; // good behaviour
+	[coin1_s2_p2] v1=2 -> true; // good behaviour
+	[coin1_s1_p1] v1=2 -> (c1'=1); // error
+	[coin1_s2_p1] v1=2 -> (c1'=1); // error
+	[coin1_s1_p2] v1=1 -> (c1'=1); // error
+	[coin1_s2_p2] v1=1 -> (c1'=1); // error
+
+endmodule
+
+// coins 2 and 3 are of no use as there are not enough rounds afterwards to decide
+
+// Labels
+label "one_proc_err" = (s1=5 | s2=5);
+label "one_coin_ok" = (c1=0);
--- a/resources/examples/testfiles/mdp/multiobj_dpm100.nm
+++ b/resources/examples/testfiles/mdp/multiobj_dpm100.nm
@ -0,0 +1,160 @@
+// power manager example
+mdp
+
+const int QMAX =2; // max queue size
+
+// to model the pm making a choice and then a move being made we need
+// two clock ticks for each transition
+// first the pm decides tick1 and then the system moves tick2
+
+module timer
+
+	c : [0..1];
+
+	[tick1] c=0 -> (c'=1);
+	[tick2] c=1 -> (c'=0);
+	
+endmodule
+
+//-------------------------------------------------------------------------
+
+// POWER MANAGER
+module PM
+
+	pm : [0..4] init 4;
+	// 0 - go to active 
+	// 1 - go to idle 
+	// 2 - go to idlelp 
+	// 3 - go to stby  
+	// 4 - go to sleep 
+
+	[tick1] true -> (pm'=0);
+	[tick1] true -> (pm'=1);
+	[tick1] true -> (pm'=2);
+	[tick1] true -> (pm'=3);
+	[tick1] true -> (pm'=4);
+	
+endmodule
+
+
+//-------------------------------------------------------------------------
+
+// SERVICE REQUESTER
+module SR
+
+	sr : [0..1] init 0;
+	// 0 idle
+	// 1 1req
+	
+	[tick2] sr=0 -> 0.898: (sr'=0) + 0.102: (sr'=1);
+	[tick2] sr=1 -> 0.454: (sr'=0) + 0.546: (sr'=1);
+
+endmodule
+
+//-------------------------------------------------------------------------
+
+// SERVICE PROVIDER
+
+module SP 
+
+	sp : [0..10] init 9;
+	// 0 active
+	// 1 idle
+	// 2 active_idlelp
+	// 3 idlelp
+	// 4 idlelp_active
+	// 5 active_stby
+	// 6 stby
+	// 7 stby_active
+    // 8 active_sleep
+	// 9 sleep
+	// 10 sleep_active
+	
+	// states where PM has no control (transient states)
+	[tick2] sp=2  ->   0.75   : (sp'=2) + 0.25   : (sp'=3);   // active_idlelp
+	[tick2] sp=4  ->   0.25   : (sp'=0) + 0.75   : (sp'=4);  // idlelp_active
+	[tick2] sp=5  ->   0.995  : (sp'=5) + 0.005  : (sp'=6);  // active_stby
+	[tick2] sp=7  ->   0.005  : (sp'=0) + 0.995  : (sp'=7);  // stby_active
+	[tick2] sp=8  ->   0.9983 : (sp'=8) + 0.0017 : (sp'=9);  // active_sleep
+	[tick2] sp=10 ->   0.0017 : (sp'=0) + 0.9983 : (sp'=10); // sleep_active
+
+	// states where PM has control
+	// goto_active
+	[tick2] sp=0 & pm=0 -> (sp'=0); // active
+	[tick2] sp=1 & pm=0 -> (sp'=0); // idle
+	[tick2] sp=3 & pm=0 -> (sp'=4); // idlelp
+	[tick2] sp=6 & pm=0 -> (sp'=7); // stby
+	[tick2] sp=9 & pm=0 -> (sp'=10); // sleep
+	// goto_idle
+	[tick2] sp=0 & pm=1 -> (sp'=1); // active
+	[tick2] sp=1 & pm=1 -> (sp'=1); // idle
+	[tick2] sp=3 & pm=1 -> (sp'=3); // idlelp
+	[tick2] sp=6 & pm=1 -> (sp'=6); // stby
+	[tick2] sp=9 & pm=1 -> (sp'=9); // sleep
+	// goto_idlelp
+	[tick2] sp=0 & pm=2 -> (sp'=2); // active
+	[tick2] sp=1 & pm=2 -> (sp'=2); // idle
+	[tick2] sp=3 & pm=2 -> (sp'=3); // idlelp
+	[tick2] sp=6 & pm=2 -> (sp'=6); // stby
+	[tick2] sp=9 & pm=2 -> (sp'=9); // sleep
+	// goto_stby
+	[tick2] sp=0 & pm=3 -> (sp'=5); // active
+	[tick2] sp=1 & pm=3 -> (sp'=5); // idle
+	[tick2] sp=3 & pm=3 -> (sp'=5); // idlelp
+	[tick2] sp=6 & pm=3 -> (sp'=6); // stby
+	[tick2] sp=9 & pm=3 -> (sp'=9); // sleep
+	// goto_sleep
+	[tick2] sp=0 & pm=4 -> (sp'=8); // active
+	[tick2] sp=1 & pm=4 -> (sp'=8); // idle
+	[tick2] sp=3 & pm=4 -> (sp'=8); // idlelp
+	[tick2] sp=6 & pm=4 -> (sp'=8); // stby
+	[tick2] sp=9 & pm=4 -> (sp'=9); // sleep
+	  
+endmodule
+
+
+//-------------------------------------------------------------------------
+
+// SQ
+module SQ
+
+	q : [0..QMAX] init 0;
+	
+	// serve if busy
+	[tick2] sr=0 & sp=0 -> (q'=max(q-1,0));
+	[tick2] sr=1 & sp=0 -> (q'=q);
+	
+	// otherwise do nothing
+	[tick2] sr=0 & sp>0 -> (q'=q);
+	[tick2] sr=1 & sp>0 -> (q'=min(q+1,QMAX));
+
+endmodule
+
+//-------------------------------------------------------------------------
+//rewards "time"
+//	[tick2] bat=1 : 1;
+//endrewards
+
+rewards "power"
+	[tick2] sp=0  & c=1  : 2.5;
+	[tick2] sp=1  & c=1  : 1.5;
+	[tick2] sp=2  & c=1  : 2.5;
+	[tick2] sp=3  & c=1  : 0.8;
+	[tick2] sp=4  & c=1  : 2.5;
+	[tick2] sp=5  & c=1  : 2.5;
+	[tick2] sp=6  & c=1  : 0.3;
+	[tick2] sp=7  & c=1  : 2.5;
+	[tick2] sp=8  & c=1  : 2.5;
+	[tick2] sp=9  & c=1  : 0.1;
+	[tick2] sp=10 & c=1  : 2.5;
+endrewards
+
+// is an instantaneous property but I suppose we can look at average size
+// i.e. divide by the expected number of time steps
+rewards "queue"
+	[tick2] c=1  : q;
+endrewards
+
+rewards "lost"
+	[tick2] sr=1 & sp>0 & q=2  : 1;
+endrewards
--- a/resources/examples/testfiles/mdp/multiobj_scheduler05.nm
+++ b/resources/examples/testfiles/mdp/multiobj_scheduler05.nm
@ -0,0 +1,95 @@
+mdp
+
+label "tasks_complete" = (task6=3);
+
+const int K=5;
+
+module scheduler
+
+	task1 : [0..3];
+	task2 : [0..3];
+	task3 : [0..3];
+	task4 : [0..3];
+	task5 : [0..3];
+	task6 : [0..3];
+
+	[p1_add] task1=0 -> (task1'=1);
+	[p2_add] task1=0 -> (task1'=2);
+	[p1_mult] task2=0 -> (task2'=1);
+	[p2_mult] task2=0 -> (task2'=2);
+	[p1_mult] task3=0&task1=3 -> (task3'=1);
+	[p2_mult] task3=0&task1=3 -> (task3'=2);
+	[p1_add] task4=0&task1=3&task2=3 -> (task4'=1);
+	[p2_add] task4=0&task1=3&task2=3 -> (task4'=2);
+	[p1_mult] task5=0&task3=3 -> (task5'=1);
+	[p2_mult] task5=0&task3=3 -> (task5'=2);
+	[p1_add] task6=0&task4=3&task5=3 -> (task6'=1);
+	[p2_add] task6=0&task4=3&task5=3 -> (task6'=2);
+	[p1_done] task1=1 -> (task1'=3);
+	[p1_done] task2=1 -> (task2'=3);
+	[p1_done] task3=1 -> (task3'=3);
+	[p1_done] task4=1 -> (task4'=3);
+	[p1_done] task5=1 -> (task5'=3);
+	[p1_done] task6=1 -> (task6'=3);
+	[p2_done] task1=2 -> (task1'=3);
+	[p2_done] task2=2 -> (task2'=3);
+	[p2_done] task3=2 -> (task3'=3);
+	[p2_done] task4=2 -> (task4'=3);
+	[p2_done] task5=2 -> (task5'=3);
+	[p2_done] task6=2 -> (task6'=3);
+	[time] true -> 1.0 : true;
+
+endmodule
+
+module P1
+
+	p1 : [0..3];
+	c1 : [0..2];
+	x1 : [0..4*K+1];
+
+	[p1_add] (p1=0) -> (p1'=1) & (x1'=0);
+	[] (p1=1)&(x1=1*K)&(c1=0) -> 1/3 : (p1'=3) & (x1'=0) & (c1'=0) + 2/3 : (c1'=1) & (x1'=0);
+	[] (p1=1)&(x1=1*K)&(c1=1) -> 1/2 : (p1'=3) & (x1'=0) & (c1'=0) + 1/2 : (c1'=2) & (x1'=0);
+	[p1_done] (p1=1)&(x1=1*K)&(c1=2) -> (p1'=0) & (x1'=0) & (c1'=0);
+	[p1_mult] (p1=0) -> (p1'=2) & (x1'=0);
+	[] (p1=2)&(x1=2*K)&(c1=0) -> 1/3 : (p1'=3) & (x1'=0) & (c1'=0) + 2/3 : (c1'=1) & (x1'=0);
+	[] (p1=2)&(x1=1*K)&(c1=1) -> 1/2 : (p1'=3) & (x1'=0) & (c1'=0) + 1/2 : (c1'=2) & (x1'=0);
+	[p1_done] (p1=2)&(x1=1*K)&(c1=2) -> (p1'=0) & (x1'=0) & (c1'=0);
+	[p1_done] (p1=3) -> (p1'=0);
+	[time] (p1=1=>x1+1<=1*K)&((p1=2&c1=0)=>x1+1<=2*K)&((p1=2&c1>0)=>x1+1<=1*K)&(p1=3=>x1+1<=0) -> 1.0 : (x1'=min(x1+1,4*K+1));
+
+endmodule
+
+module P2
+
+	p2 : [0..3];
+	c2 : [0..2];
+	x2 : [0..6*K+1];
+
+	[p2_add] (p2=0) -> (p2'=1) & (x2'=0);
+	[] (p2=1)&(x2=4*K)&(c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0);
+	[] (p2=1)&(x2=1)&(c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0);
+	[p2_done] (p2=1)&(x2=1)&(c2=2) -> (p2'=0) & (x2'=0) & (c2'=0);
+	[p2_mult] (p2=0) -> (p2'=2) & (x2'=0);
+	[] (p2=2)&(x2=6*K)&(c2=0) -> 1/3 : (p2'=3) & (x2'=0) & (c2'=0) + 2/3 : (c2'=1) & (x2'=0);
+	[] (p2=2)&(x2=1)&(c2=1) -> 1/2 : (p2'=3) & (x2'=0) & (c2'=0) + 1/2 : (c2'=2) & (x2'=0);
+	[p2_done] (p2=2)&(x2=1)&(c2=2) -> (p2'=0) & (x2'=0) & (c2'=0);
+	[p2_done] (p2=3) -> (p2'=0);
+	[time] ((p2=1&c2=0)=>x2+1<=4*K)&((p2=1&c2>0)=>x2+1<=1)&((p2=2&c2=0)=>x2+1<=6*K)&((p2=2&c2>0)=>x2+1<=1)&(p2=3=>x2+1<=0) -> 1.0 : (x2'=min(x2+1,6*K+1));
+
+endmodule
+
+rewards "time" 
+
+	[time] true : 1/K;
+
+endrewards
+
+rewards "energy" 
+
+	[time] p1=0 : 10/(1000*K);
+	[time] p1>0 : 90/(1000*K);
+	[time] p2=0 : 20/(1000*K);
+	[time] p2>0 : 30/(1000*K);
+
+endrewards
--- a/resources/examples/testfiles/mdp/multiobj_team3.nm
+++ b/resources/examples/testfiles/mdp/multiobj_team3.nm
@ -0,0 +1,288 @@
+mdp
+
+// parameters
+const int n_resources = 3;
+const int n_tasks = 2;
+const int n_sensors = 3;
+
+
+// sensor resources
+const int resource1=1;
+const int resource2=2;
+const int resource3=3;
+
+// network configuration
+const int e12=1;
+const int e13=1;
+
+const int e21=e12;
+const int e23=1;
+
+const int e31=e13;
+const int e32=e23;
+
+
+
+
+// agent is committed to some team
+formula committed = (m1_t1+m1_t2) > 0;
+
+// formulae to compute team sizes
+formula team_size_t1 = m1_t1+m2_t1+m3_t1;
+formula team_size_t2 = m1_t2+m2_t2+m3_t2;
+
+// formulae to check whether the agent can join the team
+formula can_join_t1 = e12*m2_t1 + e13*m3_t1 > 0;
+formula can_join_t2 = e12*m2_t2 + e13*m3_t2  > 0;
+
+// formulae to check whether agent has the resource required by the task
+formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
+formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
+
+// formulae to check whether the resource of an agent has been already filled in the team
+formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3);
+formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3);
+
+// formula to compute team initiation probability (assuming each agent has at least one connection)
+formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))) / (e12+e13);
+
+
+module controller // schedules the algorithm
+
+	// algorithm status
+	status : [0..6];
+
+	// task resource indicator variables
+	t1_r1 : [0..1];
+	t1_r2 : [0..1];
+	t1_r3 : [0..1];
+	
+	t2_r1 : [0..1];
+	t2_r2 : [0..1];
+	t2_r3 : [0..1];
+
+	// schedule placeholders
+	turn1 : [0..n_sensors];
+	turn2 : [0..n_sensors];
+	turn3 : [0..n_sensors];
+
+	// selecting schedule uniformly at random
+	[] status=0 -> 1/6 : (turn1'=1) & (turn2'=2) & (turn3'=3) & (status'=1)
+		 + 1/6 : (turn1'=1) & (turn2'=3) & (turn3'=2) & (status'=1)
+		 + 1/6 : (turn1'=2) & (turn2'=1) & (turn3'=3) & (status'=1)
+		 + 1/6 : (turn1'=2) & (turn2'=3) & (turn3'=1) & (status'=1)
+		 + 1/6 : (turn1'=3) & (turn2'=1) & (turn3'=2) & (status'=1)
+		 + 1/6 : (turn1'=3) & (turn2'=2) & (turn3'=1) & (status'=1);
+
+
+	// initialising non-empty tasks uniformly at random
+	[] status=1 -> 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=0) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=0) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=0) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=0) & (t2_r2'=1) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=0) & (t2_r3'=1) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=0) & (status'=2)
+		 + 1/49 : (t1_r1'=1) & (t1_r2'=1) & (t1_r3'=1) & (t2_r1'=1) & (t2_r2'=1) & (t2_r3'=1) & (status'=2);
+
+	// executing the schedule
+
+	// 1st round
+	[str1] status=2 & turn1=1 -> (status'=2);
+	[fin1] status=2 & turn1=1 -> (status'=3);
+	[str2] status=2 & turn1=2 -> (status'=2);
+	[fin2] status=2 & turn1=2 -> (status'=3);
+	[str3] status=2 & turn1=3 -> (status'=2);
+	[fin3] status=2 & turn1=3 -> (status'=3);
+
+	// 2nd round
+	[str1] status=3 & turn2=1 -> (status'=3);
+	[fin1] status=3 & turn2=1 -> (status'=4);
+	[str2] status=3 & turn2=2 -> (status'=3);
+	[fin2] status=3 & turn2=2 -> (status'=4);
+	[str3] status=3 & turn2=3 -> (status'=3);
+	[fin3] status=3 & turn2=3 -> (status'=4);
+
+	// 3rd round
+	[str1] status=4 & turn3=1 -> (status'=4);
+	[fin1] status=4 & turn3=1 -> (status'=5);
+	[str2] status=4 & turn3=2 -> (status'=4);
+	[fin2] status=4 & turn3=2 -> (status'=5);
+	[str3] status=4 & turn3=3 -> (status'=4);
+	[fin3] status=4 & turn3=3 -> (status'=5);
+
+	[] status=5 -> (status'=6);
+
+	[] status=6 -> true;
+
+endmodule
+
+module sensor1
+
+	state1 : [0..1];
+
+	// team membership indicators
+	m1_t1 : [0..1];
+	m1_t2 : [0..1];
+
+	// starting turn, selecting order of tasks
+	[str1] state1=0 -> (state1'=1);
+
+	// if there is no team and has required skill - initiating the team
+	[] state1=1 & !committed & team_size_t1=0 & has_resource_t1 -> (m1_t1'=1);
+	[] state1=1 & !committed & team_size_t2=0 & has_resource_t2 -> (m1_t2'=1);
+
+	// if team already exists and one of the neighbours is in it - joining the team 
+	[] state1=1 & !committed & team_size_t1>0 & can_join_t1 & has_resource_t1 & !resource_filled_t1 -> (m1_t1'=1);
+	[] state1=1 & !committed & team_size_t2>0 & can_join_t2 & has_resource_t2 & !resource_filled_t2 -> (m1_t2'=1);
+	
+	[fin1] state1>0 -> (state1'=0); 
+
+endmodule
+
+module sensor2 = sensor1 
+[ 
+	state1=state2, 
+
+	str1=str2,
+	fin1=fin2,
+
+	m1_t1=m2_t1,
+	m1_t2=m2_t2,
+
+	m2_t1=m1_t1,
+	m2_t2=m1_t2,
+
+	resource1=resource2,	
+	resource2=resource1,
+
+	e12=e21,
+	e13=e23,
+	e14=e24,
+	e15=e25,
+
+	e21=e12,
+	e23=e13,
+	e24=e14,
+	e25=e15
+] 
+endmodule
+
+module sensor3 = sensor1 
+[ 
+	state1=state3, 
+
+	str1=str3,
+	fin1=fin3,
+
+	m1_t1=m3_t1,
+	m1_t2=m3_t2,
+	m3_t1=m1_t1,
+	m3_t2=m1_t2,
+
+	resource1=resource3,	
+	resource3=resource1,
+
+	e12=e32,
+	e13=e31,
+	e14=e34,
+	e15=e35,
+
+	e31=e13,
+	e32=e12,
+	e34=e14,
+	e35=e15
+] 
+endmodule
+
+
+
+
+// labels and formulae for property specification 
+formula finished = (status=5);
+label "end" = (status=6);
+
+
+formula task1_completed = finished 
+		 	 & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)))
+			 & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)))
+			 & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)));
+
+formula task2_completed = finished
+			 & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)))
+			 & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)))
+			 & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)));
+
+
+
+formula agent1_joins_successful_team = (task1_completed & m1_t1=1) | (task2_completed & m1_t2=1);
+formula agent1_joins_successful_team_of_1 = (task1_completed & m1_t1=1 & team_size_t1=1) | (task2_completed & m1_t2=1 & team_size_t2=1);
+formula agent1_joins_successful_team_of_2 = (task1_completed & m1_t1=1 & team_size_t1=2) | (task2_completed & m1_t2=1 & team_size_t2=2);
+formula agent1_joins_successful_team_of_3 = (task1_completed & m1_t1=1 & team_size_t1=3) | (task2_completed & m1_t2=1 & team_size_t2=3);
+
+formula agent2_joins_successful_team = (task1_completed & m2_t1=1) | (task2_completed & m2_t2=1);
+formula agent2_joins_successful_team_of_1 = (task1_completed & m2_t1=1 & team_size_t1=1) | (task2_completed & m2_t2=1 & team_size_t2=1);
+formula agent2_joins_successful_team_of_2 = (task1_completed & m2_t1=1 & team_size_t1=2) | (task2_completed & m2_t2=1 & team_size_t2=2);
+formula agent2_joins_successful_team_of_3 = (task1_completed & m2_t1=1 & team_size_t1=3) | (task2_completed & m2_t2=1 & team_size_t2=3);
+
+formula agent3_joins_successful_team = (task1_completed & m3_t1=1) | (task2_completed & m3_t2=1);
+formula agent3_joins_successful_team_of_1 = (task1_completed & m3_t1=1 & team_size_t1=1) | (task2_completed & m3_t2=1 & team_size_t2=1);
+formula agent3_joins_successful_team_of_2 = (task1_completed & m3_t1=1 & team_size_t1=2) | (task2_completed & m3_t2=1 & team_size_t2=2);
+formula agent3_joins_successful_team_of_3 = (task1_completed & m3_t1=1 & team_size_t1=3) | (task2_completed & m3_t2=1 & team_size_t2=3);
+
+// rewards
+rewards "w_1_total"
+    [] agent1_joins_successful_team : 1;
+    [] agent2_joins_successful_team : 1;
+    [] agent3_joins_successful_team : 1;
+endrewards
+
+rewards "w_2_total"
+    [] task1_completed : 1;
+    [] task2_completed : 1;
+endrewards
+
+
+
+
--- a/resources/examples/testfiles/mdp/multiobj_zeroconf4.nm
+++ b/resources/examples/testfiles/mdp/multiobj_zeroconf4.nm
@ -0,0 +1,153 @@
+// IPv4: PTA model with digitial clocks
+// multi-objective model of the host
+// gxn/dxp 28/09/09
+
+mdp
+
+//-------------------------------------------------------------
+// VARIABLES
+const int N=20; // number of abstract hosts
+const int K=4; // number of probes to send
+
+// PROBABILITIES
+const double old = N/65024; // probability pick an ip address being used
+//const double old = 0.5; // probability pick an ip address being used
+const double new = (1-old); // probability pick a new ip address
+
+// TIMING CONSTANTS
+const int CONSEC = 2;  // time interval between sending consecutive probles 
+const int TRANSTIME = 1; // upper bound on transmission time delay
+const int LONGWAIT = 60; // minimum time delay after a high number of address collisions
+const int DEFEND = 10;
+
+const int TIME_MAX_X = 60; // max value of clock x
+const int TIME_MAX_Y = 10; // max value of clock y
+const int TIME_MAX_Z = 1;  // max value of clock z
+
+// OTHER CONSTANTS
+const int MAXCOLL = 10;  // maximum number of collisions before long wait
+const int M=1; // time between sending and receiving a message
+
+
+//-------------------------------------------------------------
+// CONCRETE HOST
+module host0
+	
+	x : [0..TIME_MAX_X]; // first clock of the host
+	y : [0..TIME_MAX_Y]; // second clock of the host
+	
+	coll : [0..MAXCOLL]; // number of address collisions
+	probes : [0..K]; // counter (number of probes sent)
+	mess : [0..1]; // need to send a message or not
+	defend : [0..1]; // defend (if =1, try to defend IP address)
+	
+	ip : [1..2]; // ip address (1 - in use & 2 - fresh)
+	
+	l : [0..4] init 1; // location
+	// 0 : RECONFIGURE 
+	// 1 : RANDOM
+	// 2 : WAITSP
+	// 3 : WAITSG 
+	// 4 : USE
+	
+	// RECONFIGURE
+	[reset] l=0 -> (l'=1);
+	
+	// RANDOM (choose IP address)
+	[rec0] (l=1) -> true; // get message (ignore since have no ip address)
+	[rec1] (l=1) -> true; // get message (ignore since have no ip address)
+	// small number of collisions (choose straight away)
+	[] l=1 & coll<MAXCOLL -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) 
+		                     + 1/3*old : (l'=2) & (ip'=1) & (x'=1) 
+		                     + 1/3*old : (l'=2) & (ip'=1) & (x'=2) 
+		                     + 1/3*new : (l'=2) & (ip'=2) & (x'=0) 
+		                     + 1/3*new : (l'=2) & (ip'=2) & (x'=1) 
+		                     + 1/3*new : (l'=2) & (ip'=2) & (x'=2); 
+	// large number of collisions: (wait for LONGWAIT)
+	[time] l=1 & coll=MAXCOLL & x<LONGWAIT -> (x'=min(x+1,TIME_MAX_X));
+	[]     l=1 & coll=MAXCOLL & x=LONGWAIT -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) 
+			                                   + 1/3*old : (l'=2) & (ip'=1) & (x'=1) 
+			                                   + 1/3*old : (l'=2) & (ip'=1) & (x'=2) 
+			                                   + 1/3*new : (l'=2) & (ip'=2) & (x'=0) 
+			                                   + 1/3*new : (l'=2) & (ip'=2) & (x'=1) 
+			                                   + 1/3*new : (l'=2) & (ip'=2) & (x'=2);
+	
+	// WAITSP 
+	// let time pass
+	[time]  l=2 & x<2 -> (x'=min(x+1,2));
+	// send probe
+	[send1] l=2 & ip=1 & x=2  & probes<K -> (x'=0) & (probes'=probes+1);
+	[send2] l=2 & ip=2 & x=2  & probes<K -> (x'=0) & (probes'=probes+1);
+	// sent K probes and waited 2 seconds
+	[] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
+	// get message and ip does not match: ignore
+	[rec0] l=2 & ip!=0 -> (l'=l);
+	[rec1] l=2 & ip!=1 -> (l'=l);
+	// get a message with matching ip: reconfigure
+	[rec1] l=2 & ip=1 -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0);
+	
+	// WAITSG (sends two gratuitious arp probes)
+	// time passage
+	[time] l=3 & mess=0 & defend=0 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)); 
+	[time] l=3 & mess=0 & defend=1 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)) & (y'=min(y+1,DEFEND));
+	
+	// receive message and same ip: defend
+	[rec1] l=3 & mess=0 & ip=1 & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
+	// receive message and same ip: defer
+	[rec1] l=3 & mess=0 & ip=1 & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
+	// receive message and different ip
+	[rec0] l=3 & mess=0 & ip!=0 -> (l'=l);
+	[rec1] l=3 & mess=0 & ip!=1 -> (l'=l);
+	
+		
+	// send probe reply or message for defence
+	[send1] l=3 & ip=1 & mess=1 -> (mess'=0);
+	[send2] l=3 & ip=2 & mess=1 -> (mess'=0);
+	// send first gratuitous arp message
+	[send1] l=3 & ip=1 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
+	[send2] l=3 & ip=2 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
+	// send second gratuitous arp message (move to use)
+	[send1] l=3 & ip=1 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
+	[send2] l=3 & ip=2 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0);
+	
+	// USE (only interested in reaching this state so do not need to add anything here)
+	[] l=4 -> true;
+	
+endmodule
+
+//-------------------------------------------------------------
+// error automaton for the environment assumption
+// do not get a reply when K probes are sent
+
+module env_error4
+
+	env : [0..1]; // 0 active and 1 done
+	k : [0..4]; // counts the number of messages sent
+	c1 : [0..M+1]; // time since first message
+	c2 : [0..M+1]; // time since second message
+	c3 : [0..M+1]; // time since third message
+	c4 : [0..M+1]; // time since fourth message
+	error : [0..1];
+
+	// message with new ip address arrives so done
+	[send2] error=0 & env=0 -> (env'=1);
+	// message with old ip address arrives so count
+	[send1] error=0 & env=0 -> (k'=min(k+1,K));
+	// time passgae so update relevant clocks
+	[time] error=0 & env=0 & k=0 -> true;
+	[time] error=0 & env=0 & k=1 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1));
+	[time] error=0 & env=0 & k=2 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1));
+	[time] error=0 & env=0 & k=3 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1)) & (c3'=min(c3+1,M+1));
+	[time] error=0 & env=0 & k=4 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1)) & (c3'=min(c3+1,M+1)) & (c4'=min(c4+1,M+1));
+	// all clocks reached their bound so an error
+	[time] error=0 & env=0 & min(c1,c2,c3,c4)=M -> (error'=1); 
+	// send a reply (then done)
+	[rec1] error=0 & env=0 & k>0 & min(c1,c2,c3,c4)<=M -> (env'=1);
+	// finished so any action can be performed
+	[time]  error=1 | env=1 -> true;
+	[send1]  error=1 | env=1 -> true;
+	[send2]  error=1 | env=1 -> true;
+	[send2]  error=1 | env=1 -> true;
+	[rec1]  error=1 | env=1 -> true;
+
+endmodule
--- a/resources/examples/testfiles/mdp/multiobjective1.nm
+++ b/resources/examples/testfiles/mdp/multiobjective1.nm
@ -1,20 +0,0 @@
- 
-mdp
-
-module module1
-
-	// local state
-	s : [0..2] init 0;
-
-	[A] s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2);
-	[B] s=0 -> 0.3 : (s'=0) + 0.7 : (s'=1);
-	[C] s=0 -> 0.2 : (s'=0) + 0.8 : (s'=2);
-	[D] s=1 -> 0.25 : (s'=0) + 0.75 : (s'=2); 
-	[]  s=2 -> 1 : (s'=s);
-endmodule
-
-rewards "rew"
-	[A] true : 10;
-	[D] true : 4;
-endrewards
-
--- a/resources/examples/testfiles/mdp/multiobjective2.nm
+++ b/resources/examples/testfiles/mdp/multiobjective2.nm
@ -1,20 +0,0 @@
- 
-mdp
-
-module module1
-
-	s : [0..2] init 0;
-
-	[A] s=0 -> 1 : (s'=1);
-	[B] s=0  -> 1 : (s'=2);
-	[C] s=1 -> 1 : true;
-	[D] s=1 -> 1 : (s'=2);
-	[E] s=2 -> 1 : true;
-endmodule
-
-rewards "rew"
-	[A] true : 10;
-	[C] true : 3;
-	[E] true : 1;
-endrewards
-
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@ -1,3 +1,7 @@
+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+
 add_subdirectory(storm)
 add_subdirectory(storm-pgcl)
 add_subdirectory(storm-pgcl-cli)
--- a/src/storm/adapters/NumberAdapter.h
+++ b/src/storm/adapters/NumberAdapter.h
@ -6,7 +6,7 @@

 #include <carl/numbers/numbers.h>
 namespace storm {
-#if defined STORM_HAVE_CLN && defined USE_CLN_NUMBERS
+#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_NUMBERS
    typedef cln::cl_RA RationalNumber;
 #else
    typedef mpq_class RationalNumber;
--- a/src/storm/solver/stateelimination/ConditionalStateEliminator.cpp
+++ b/src/storm/solver/stateelimination/ConditionalStateEliminator.cpp
@ -13,12 +13,12 @@ namespace storm {
            
            template<typename ValueType>
            void ConditionalStateEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
-                oneStepProbabilities[state] = storm::utility::simplify(loopProbability * oneStepProbabilities[state]);
+                oneStepProbabilities[state] = storm::utility::simplify((ValueType) (loopProbability * oneStepProbabilities[state]));
            }
            
            template<typename ValueType>
            void ConditionalStateEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
-                oneStepProbabilities[predecessor] = storm::utility::simplify(oneStepProbabilities[predecessor] * storm::utility::simplify(probability * oneStepProbabilities[state]));
+                oneStepProbabilities[predecessor] = storm::utility::simplify((ValueType) (oneStepProbabilities[predecessor] * storm::utility::simplify((ValueType) (probability * oneStepProbabilities[state]))));
            }
                        
            template<typename ValueType>
--- a/src/storm/solver/stateelimination/EliminatorBase.cpp
+++ b/src/storm/solver/stateelimination/EliminatorBase.cpp
@ -58,8 +58,7 @@ namespace storm {
                    for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); entryIt != entryIte; ++entryIt) {
                        // Only scale the entries in a different column.
                        if (entryIt->getColumn() != column) {
-                            auto tmpVal = entryIt->getValue() * columnValue;
-                            entryIt->setValue(storm::utility::simplify(tmpVal));
+                            entryIt->setValue(storm::utility::simplify((ValueType) (entryIt->getValue() * columnValue)));
                        }
                    }
                    updateValue(column, columnValue);
--- a/src/storm/solver/stateelimination/MultiValueStateEliminator.cpp
+++ b/src/storm/solver/stateelimination/MultiValueStateEliminator.cpp
@ -18,17 +18,17 @@ namespace storm {

            template<typename ValueType>
            void MultiValueStateEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
-                this->stateValues[state] = storm::utility::simplify(loopProbability * this->stateValues[state]);
+                this->stateValues[state] = storm::utility::simplify((ValueType) (loopProbability * this->stateValues[state]));
                for(auto additionalStateValueVectorRef : additionalStateValues) {
-                    additionalStateValueVectorRef.get()[state] = storm::utility::simplify(loopProbability * additionalStateValueVectorRef.get()[state]);
+                    additionalStateValueVectorRef.get()[state] = storm::utility::simplify((ValueType) (loopProbability * additionalStateValueVectorRef.get()[state]));
                }
            }
-       
+
            template<typename ValueType>
            void MultiValueStateEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
-                this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state]));
+                this->stateValues[predecessor] = storm::utility::simplify((ValueType) (this->stateValues[predecessor] + storm::utility::simplify((ValueType) (probability * this->stateValues[state]))));
                for(auto additionalStateValueVectorRef : additionalStateValues) {
-                    additionalStateValueVectorRef.get()[predecessor] = storm::utility::simplify(additionalStateValueVectorRef.get()[predecessor] + storm::utility::simplify(probability * additionalStateValueVectorRef.get()[state]));
+                    additionalStateValueVectorRef.get()[predecessor] = storm::utility::simplify((ValueType) (additionalStateValueVectorRef.get()[predecessor] + storm::utility::simplify((ValueType) (probability * additionalStateValueVectorRef.get()[state]))));
                }
            }

@ -39,7 +39,7 @@ namespace storm {
                    additionStateValueVectorRef.get()[state] = storm::utility::zero<ValueType>();
                }
            }
-            
+
            template class MultiValueStateEliminator<double>;

 #ifdef STORM_HAVE_CARL
--- a/src/storm/solver/stateelimination/PrioritizedStateEliminator.cpp
+++ b/src/storm/solver/stateelimination/PrioritizedStateEliminator.cpp
@ -22,12 +22,12 @@ namespace storm {
            
            template<typename ValueType>
            void PrioritizedStateEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
-                stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]);
+                stateValues[state] = storm::utility::simplify((ValueType) (loopProbability * stateValues[state]));
            }
       
            template<typename ValueType>
            void PrioritizedStateEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
-                stateValues[predecessor] = storm::utility::simplify(stateValues[predecessor] + storm::utility::simplify(probability * stateValues[state]));
+                stateValues[predecessor] = storm::utility::simplify((ValueType) (stateValues[predecessor] + storm::utility::simplify((ValueType) (probability * stateValues[state]))));
            }
            
            template<typename ValueType>
--- a/src/storm/storage/geometry/Halfspace.h
+++ b/src/storm/storage/geometry/Halfspace.h
@ -41,7 +41,7 @@ namespace storm {
                 * In contrast to the euclideanDistance method, there are no inaccuracies introduced (providing ValueType is exact for +, -, and *)
                 */
                ValueType distance(std::vector<ValueType> const& point) const {
-                    return std::max(storm::utility::zero<ValueType>(), storm::utility::vector::dotProduct(point, normalVector()) - offset());
+                    return std::max(storm::utility::zero<ValueType>(), (ValueType) (storm::utility::vector::dotProduct(point, normalVector()) - offset()));
                }
                
                /*
--- a/src/storm/utility/constants.cpp
+++ b/src/storm/utility/constants.cpp
@ -312,10 +312,10 @@ namespace storm {
        RationalNumber convertNumber(double const& number){
            return carl::rationalize<RationalNumber>(number);
        }
-        
+
        template<>
        RationalNumber convertNumber(uint_fast64_t const& number){
-            return RationalNumber(number);
+            return carl::rationalize<RationalNumber>(number);
        }

        template<>
--- a/src/storm/utility/vector.h
+++ b/src/storm/utility/vector.h
@ -396,7 +396,7 @@ namespace storm {
             */
            template<class ValueType1, class ValueType2>
            void scaleVectorInPlace(std::vector<ValueType1>& target, ValueType2 const& factor) {
-                applyPointwise<ValueType1, ValueType2>(target, target, [&] (ValueType1 const& argument) -> ValueType1 { return argument * factor; });
+                applyPointwise<ValueType1, ValueType1>(target, target, [&] (ValueType1 const& argument) -> ValueType1 { return argument * factor; });
            }
            
            /*!
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@ -17,8 +17,7 @@ foreach (testsuite abstraction adapter builder logic modelchecker parser permiss
 	  target_link_libraries(test-${testsuite} ${STORM_TEST_LINK_LIBRARIES})

 	  add_dependencies(test-${testsuite} test-resources)
-	  add_test(run-test-${testsuite} test-${testsuite})
-	  add_dependencies(check test-${testsuite})
-	  add_dependencies(check-verbose test-${testsuite})
+	  add_test(NAME run-test-${testsuite} COMMAND $<TARGET_FILE:test-${testsuite}>)
+      add_dependencies(tests test-${testsuite})
 	
 endforeach ()
--- a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp
+++ b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp
@ -58,7 +58,7 @@ TEST(SparseMaPcaaModelCheckerTest, server) {
    storm::prism::Program program = storm::parseProgram(programFile);
    program = storm::utility::prism::preprocess(program, "");
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::MarkovAutomaton<double>>();
+    std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
    storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<double>> checker(*ma);
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula());
--- a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp
+++ b/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp
@ -14,7 +14,7 @@

 TEST(SparseMdpPcaaModelCheckerTest, consensus) {
    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/consensus2_3_2.nm";
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.nm";
    std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical
    formulasAsString += "; \n multi(P>=0.1 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (true)
    formulasAsString += "; \n multi(P>=0.11 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (false)
@ -23,7 +23,7 @@ TEST(SparseMdpPcaaModelCheckerTest, consensus) {
    storm::prism::Program program = storm::parseProgram(programFile);
    program = storm::utility::prism::preprocess(program, "");
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
    uint_fast64_t const initState = *mdp->getInitialStates().begin();;
    
    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@ -44,14 +44,14 @@ TEST(SparseMdpPcaaModelCheckerTest, consensus) {

 TEST(SparseMdpPcaaModelCheckerTest, zeroconf) {
    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf4.nm";
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_zeroconf4.nm";
    std::string formulasAsString = "multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical
    
    // programm, model,  formula
    storm::prism::Program program = storm::parseProgram(programFile);
    program = storm::utility::prism::preprocess(program, "");
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
    uint_fast64_t const initState = *mdp->getInitialStates().begin();
    
    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@ -63,14 +63,14 @@ TEST(SparseMdpPcaaModelCheckerTest, zeroconf) {

 TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) {
    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/team3obj_3.nm";
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm";
    std::string formulasAsString = "multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ],  P>=0.5 [ F task2_completed ])"; // numerical
    
    // programm, model,  formula
    storm::prism::Program program = storm::parseProgram(programFile);
    program = storm::utility::prism::preprocess(program, "");
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
    uint_fast64_t const initState = *mdp->getInitialStates().begin();
    
    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@ -82,14 +82,14 @@ TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) {

 TEST(SparseMdpPcaaModelCheckerTest, scheduler) {
    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/scheduler05.nm";
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_scheduler05.nm";
    std::string formulasAsString = "multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [  F \"tasks_complete\" ]) ";
    
    // programm, model,  formula
    storm::prism::Program program = storm::parseProgram(programFile);
    program = storm::utility::prism::preprocess(program, "");
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
    uint_fast64_t const initState = *mdp->getInitialStates().begin();
    
    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
@ -100,21 +100,21 @@ TEST(SparseMdpPcaaModelCheckerTest, scheduler) {

 TEST(SparseMdpPcaaModelCheckerTest, dpm) {
    
-    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/dpm100.nm";
+    std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_dpm100.nm";
    std::string formulasAsString = "multi(R{\"power\"}min=? [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // numerical
    
    // programm, model,  formula
    storm::prism::Program program = storm::parseProgram(programFile);
    program = storm::utility::prism::preprocess(program, "");
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
-    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas, true)->as<storm::models::sparse::Mdp<double>>();
+    std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
    uint_fast64_t const initState = *mdp->getInitialStates().begin();
    
    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
    
    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
    ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(121.61288420945114, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(121.61288, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
 }