fixed implies impl and added noDead-flag for MC

also added test-case for ArithmeticExpLaws

btypes_primitives/src/main/rust/btypes/src/bboolean.rs

@@ -13,7 +13,7 @@ pub trait BBooleanT: BObject + IntoBool + Copy {
     fn xor(&self, other: &Self) -> Self;
     fn and(&self, other: &Self) -> Self;
     fn not(&self) -> Self;
-    fn implies(&self, other: &Self) -> Self;
+    fn implies<F: FnOnce() -> bool>(&self, other: F) -> Self;
     fn equivalent(&self, other: &Self) -> Self;
     fn equal(&self, other: &Self) -> Self;
     fn unequal(&self, other: &Self) -> Self;
@@ -33,7 +33,7 @@ impl BBooleanT for bool {
     fn xor(&self, other: &Self) -> Self { *self ^ *other }
     fn and(&self, other: &Self) -> Self { *self && *other }
     fn not(&self) -> Self { !*self }
-    fn implies(&self, other: &Self) -> Self { !*self || *other }
+    fn implies<F: FnOnce() -> bool>(&self, other: F) -> Self { !*self || other() }
     fn equivalent(&self, other: &Self) -> Self { *self == *other }
     fn equal(&self, other: &Self) -> Self { *self == *other }
     fn unequal(&self, other: &Self) -> Self { *self != *other }

src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg

@@ -74,7 +74,7 @@ impl <machine> {
 <if(forModelChecking)>
 fn main() {
     let args: Vec\<String> = env::args().collect();
-    if args.len() != 4 { panic!("Number of arguments errorneous"); }
+    if args.len() \< 4 { panic!("Number of arguments errorneous"); }
 
     let threads = args.get(2).unwrap().parse::\<usize>().unwrap();
     if threads \<= 0 { panic!("Input for number of threads is wrong."); }
@@ -87,10 +87,21 @@ fn main() {
         _    => panic!("Input for strategy is wrong.")
     };
 
+    let mut no_dead = false;
+
+    if args.len() > 4 {
+        for arg in args.iter().skip(4) {
+            match arg.as_str() {
+                "-nodead" => no_dead = true,
+                _ => {}
+            }
+        }
+    }
+
     if threads == 1 {
-        <machine>::model_check_single_threaded(mc_type, is_caching);
+        <machine>::model_check_single_threaded(mc_type, is_caching, no_dead);
     } else {
-        <machine>::modelCheckMultiThreaded(mc_type, threads, is_caching);
+        <machine>::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead);
     }
 }
 <endif>
@@ -552,7 +563,7 @@ and(arg1, arg2) ::= <<
 >>
 
 implies(arg1, arg2) ::= <<
-<arg1>.implies(&<arg2>)
+<arg1>.implies(|| <arg2>.booleanValue())
 >>
 
 equivalent(arg1, arg2) ::= <<
@@ -895,7 +906,7 @@ fn get_invariant_dependencies(op: &'static str) -> Vec\<&str> {
     }
 }
 
-fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
+fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool) {
     let mut machine = <machine>::new();
 
     let mut all_states = HashSet::\<<machine>\>::new();
@@ -917,7 +928,7 @@ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
             println!("INVARIANT VIOLATED");
             stop_threads = true;
         }
-        if next_states.is_empty() {
+        if !no_dead && next_states.is_empty() {
             print!("DEADLOCK DETECTED");
             stop_threads = true;
         }
@@ -935,7 +946,7 @@ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
     Self::print_result(all_states.len(), num_transitions.load(Ordering::Acquire), stop_threads);
 }
 
-fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
+fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, no_dead: bool) {
     let threadPool = ThreadPool::new(threads);
 
     let machine = <machine>::new();
@@ -964,7 +975,7 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
         //println!("Thread {:?} spawning a thread", thread::current().id());
         threadPool.execute(move|| {
             let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
-            if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
+            if !no_dead && next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
 
             //println!("Thread {:?} executing", thread::current().id());
             next_states.into_iter()

src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java

@@ -7,4 +7,9 @@ public class TestOthers extends TestRS{
     public void test_SetRelationConstructs() throws Exception {
         testRSMC("SetRelationConstructs", true);
     }
+
+    @Test
+    public void test_ArithmeticExpLaws() throws Exception {
+        testRSMC("ArithmeticExpLaws", "../../../../benchmarks/model_checking/ProB/Other", true, true);
+    }
 }

src/test/java/de/hhu/stups/codegenerator/rust/TestRS.java

@@ -41,7 +41,7 @@ public class TestRS {
     }
 
     public void testRS(String machine, String machineName, String addition, boolean execute) throws Exception {
-        testRS(machine, machineName, addition, execute, false);
+        testRS(machine, machineName, addition, execute, false, false);
     }
 
     public void testRSMC(String machine) throws Exception {
@@ -49,13 +49,21 @@ public class TestRS {
     }
 
     public void testRSMC(String machine, boolean execute) throws Exception {
-        testRS(machine, machine, null, execute, true);
-        //TODO: validation of MC result
+        testRSMC(machine, null, execute);
     }
 
-    public void testRS(String machine, String machineName, String addition, boolean execute, boolean modelChecking) throws Exception {
-        Path mchPath = Paths.get(CodeGenerator.class.getClassLoader()
-                .getResource("de/hhu/stups/codegenerator/" + machine + ".mch").toURI());
+    public void testRSMC(String machine, String machinePath, boolean execute) throws Exception {
+        testRSMC(machine, machinePath, execute, false);
+    }
+
+    public void testRSMC(String machine, String machinePath, boolean execute, boolean noDead) throws Exception {
+        testRS(machine, machinePath, null, execute, true, noDead);
+    }
+
+    public void testRS(String machine, String machinePath, String addition, boolean execute, boolean modelChecking, boolean noDead) throws Exception {
+        if (machinePath == null) { machinePath = "../../../resources/test/de/hhu/stups/codegenerator/"; }
+        if (!machinePath.endsWith("/")) { machinePath += "/"; }
+        Path mchPath = Paths.get(CodeGenerator.class.getClassLoader().getResource("").toURI()).resolve(machinePath + machine + ".mch").normalize();
         CodeGenerator codeGenerator = new CodeGenerator();
         List<Path> rsFilePaths = codeGenerator.generate(mchPath,
                                                         GeneratorMode.RS,
@@ -101,6 +109,7 @@ public class TestRS {
 
         String progArgs = "";
         if (modelChecking) { progArgs = " -- mixed 2 true"; }
+        if (noDead) { progArgs += " -nodead"; }
 
         Process executeProcess = runtime.exec("cargo run --release --manifest-path " + mainPath.getParent().getParent().toFile().getAbsolutePath() + "/Cargo.toml" + progArgs);
         executeProcess.waitFor();

src/test/resources/de/hhu/stups/codegenerator/ArithmeticExpLaws_MC.out

+MODEL CHECKING SUCCESSFUL
+Number of States: 2650
+Number of Transitions: 7105
\ No newline at end of file