diff --git a/btypes_primitives/src/main/rust/btypes/src/bboolean.rs b/btypes_primitives/src/main/rust/btypes/src/bboolean.rs
index b1188ebb86908343e28a29db304c0f18e0e8b531..8cf67db17c1fb1e0eb751d4530716201d5f51311 100644
--- a/btypes_primitives/src/main/rust/btypes/src/bboolean.rs
+++ b/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 }
diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
index 015959be2a719d768e92332d126cf7c7dd1b923f..402081beeda547812ff9d72a8709fd6ab07e6362 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
+++ b/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()
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java b/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java
index 69a95e46b853e39e863b856d2c6e5cf1bbb2930d..6806690f4d27ac713967cb2d01334a50bd601417 100644
--- a/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java
+++ b/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);
+ }
}
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust/TestRS.java b/src/test/java/de/hhu/stups/codegenerator/rust/TestRS.java
index ad5de11f04921438e9af5765185f12d7cd429892..b329e0e2b37f4f9b35f11b62e49da778a261b5a6 100644
--- a/src/test/java/de/hhu/stups/codegenerator/rust/TestRS.java
+++ b/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();
diff --git a/src/test/resources/de/hhu/stups/codegenerator/ArithmeticExpLaws_MC.out b/src/test/resources/de/hhu/stups/codegenerator/ArithmeticExpLaws_MC.out
new file mode 100644
index 0000000000000000000000000000000000000000..498a5c8a9bb9f4e870dc9c47221432916cd395ad
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/ArithmeticExpLaws_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 2650
+Number of Transitions: 7105
\ No newline at end of file