diff --git a/btypes_primitives/src/main/rust_embedded/bmachine_mc/Cargo.toml b/btypes_primitives/src/main/rust_embedded/bmachine_mc/Cargo.toml
new file mode 100644
index 0000000000000000000000000000000000000000..f3e1f38f53a251b9c6a10844be56f9272469c070
--- /dev/null
+++ b/btypes_primitives/src/main/rust_embedded/bmachine_mc/Cargo.toml
@@ -0,0 +1,28 @@
+[package]
+name = "bmachine_mc"
+version = "0.1.0"
+edition = "2018"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+btypes = { path = "../btypes" }
+threadpool = "1.8.1"
+dashmap = "~5.1.0"
+derivative = "2.2.0"
+
+[profile.release]
+#opt-level = 3
+panic = "abort"
+#lto = 'fat'
+codegen-units = 1
+debug = true
+lto = true
+opt-level = "s"
+
+[profile.dev]
+opt-level = 0
+panic = "abort"
+
+[profile.test]
+panic = "abort"
\ No newline at end of file
diff --git a/btypes_primitives/src/main/rust_embedded/btypes/src/binteger.rs b/btypes_primitives/src/main/rust_embedded/btypes/src/binteger.rs
index 3685660e0608b2955a464b5fbc0f96a9822dd283..02f68e9edf91b63a670488bf824bf2a4ca964b7a 100644
--- a/btypes_primitives/src/main/rust_embedded/btypes/src/binteger.rs
+++ b/btypes_primitives/src/main/rust_embedded/btypes/src/binteger.rs
@@ -1,6 +1,7 @@
#![allow(non_snake_case, non_camel_case_types)]
use core::convert::TryInto;
+use crate::bboolean::BBoolean;
use crate::bset::{BSet, SetItem};
pub type BInteger = i128;
@@ -32,6 +33,13 @@ pub trait BInt {
fn from(source: BInteger) -> Self;
fn new(source: BInteger) -> Self;
+
+ fn isInteger(&self) -> BBoolean { true }
+ fn isNotInteger(&self) -> BBoolean { false }
+ fn isNatural(&self) -> BBoolean;
+ fn isNotNatural(&self) -> BBoolean;
+ fn isNatural1(&self) -> BBoolean;
+ fn isNotNatural1(&self) -> BBoolean;
}
impl BInt for BInteger {
@@ -60,6 +68,14 @@ impl BInt for BInteger {
fn from(source: BInteger) -> Self { source }
fn new(source: BInteger) -> Self { source }
+
+ fn isNatural(&self) -> BBoolean { return *self >= 0; }
+
+ fn isNotNatural(&self) -> BBoolean { return *self < 0; }
+
+ fn isNatural1(&self) -> BBoolean { return *self > 0; }
+
+ fn isNotNatural1(&self) -> BBoolean { return *self < 1; }
}
diff --git a/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs b/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
index 4c05e3a8e1d78dd928de4a1375bff46d6ca836ce..54ea195fdbf5f6b84b72323b7b1d96c14156fc98 100644
--- a/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
+++ b/btypes_primitives/src/main/rust_embedded/btypes/src/brelation.rs
@@ -106,6 +106,28 @@ impl<L, const LS: usize, R, const RS: usize, const SIZE: usize, const REL_SIZE:
}
}
+
+
+pub trait TBRelation {
+ fn isPartialInteger(&self) -> BBoolean { false }
+ fn checkDomainInteger(&self) -> BBoolean { false }
+ fn isPartialNatural(&self) -> BBoolean { false }
+ fn checkDomainNatural(&self) -> BBoolean { false }
+ fn isPartialNatural1(&self) -> BBoolean { false }
+ fn checkDomainNatural1(&self) -> BBoolean { false }
+ fn checkRangeInteger(&self) -> BBoolean { false }
+ fn checkRangeNatural(&self) -> BBoolean { false }
+ fn checkRangeNatural1(&self) -> BBoolean { false }
+ fn checkDomainString(&self) -> BBoolean { false }
+ fn isPartialString(&self) -> BBoolean { false }
+ fn checkRangeString(&self) -> BBoolean { false }
+ fn checkDomainStruct(&self) -> BBoolean { false }
+ fn isPartialStruct(&self) -> BBoolean { false }
+ fn checkRangeStruct(&self) -> BBoolean { false }
+}
+
+impl<L: SetItem<LS>, const LS: usize, R: SetItem<RS>, const RS: usize, const REL_SIZE: usize> TBRelation for BRelation<L, LS, R, RS, REL_SIZE> {}
+
impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L, LS, R, RS, REL_SIZE>
where L: SetItem<LS>,
R: SetItem<RS>{
@@ -118,6 +140,8 @@ impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L,
BRelation { rel: self.rel, _p: PhantomData, _p2: PhantomData }
}
+ pub fn iter(&self) -> BRelIter<L, LS, R, RS> { BRelIter::new(self.rel) }
+
pub fn _override_single(&self, left_item: L, right_item: R) -> Self {
let mut result = self.copy();
let left_idx = left_item.as_idx();
@@ -515,6 +539,53 @@ where L: SetItem<LS> + BInt,
}
return result;
}
+
+ pub fn isPartialInteger(&self) -> BBoolean { true }
+ pub fn checkDomainInteger(&self) -> BBoolean { return self.isPartialInteger(); }
+ pub fn isPartialNatural(&self) -> BBoolean { return self.domain().subsetOfNatural(); }
+ pub fn checkDomainNatural(&self) -> BBoolean { return self.isPartialNatural(); }
+ pub fn isPartialNatural1(&self) -> BBoolean { return self.domain().subsetOfNatural1(); }
+ pub fn checkDomainNatural1(&self) -> BBoolean { return self.isPartialNatural1(); }
+}
+
+impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L, LS, R, RS, REL_SIZE>
+where L: SetItem<LS>,
+ R: SetItem<RS> + BInt{
+ pub fn checkRangeInteger(&self) -> BBoolean { true }
+ pub fn checkRangeNatural(&self) -> BBoolean { return self.range().subsetOfNatural(); }
+ pub fn checkRangeNatural1(&self) -> BBoolean { return self.range().subsetOfNatural1(); }
+}
+
+
+pub struct BRelIter<L: SetItem<LS>, const LS: usize, R: SetItem<RS>, const RS: usize> {
+ brel: [[bool; RS]; LS],
+ c_l: usize,
+ c_r: usize,
+ _p: PhantomData<L>,
+ _p2: PhantomData<R>,
+}
+
+impl<L: SetItem<LS>, const LS: usize, R: SetItem<RS>, const RS: usize> BRelIter<L, LS, R, RS> {
+ pub const fn new(arr: [[bool; RS]; LS]) -> Self { BRelIter { brel: arr, c_l: 0, c_r: 0, _p: PhantomData, _p2: PhantomData } }
+}
+
+impl<L: SetItem<LS>, const LS: usize, R: SetItem<RS>, const RS: usize> Iterator for BRelIter<L, LS, R, RS> {
+ type Item = (L, R);
+
+ fn next(&mut self) -> Option<Self::Item> {
+ while self.c_l < LS {
+ while self.c_r < RS {
+ if self.brel[self.c_l][self.c_r] {
+ self.c_r += 1;
+ return Option::Some((L::from_idx(self.c_l), R::from_idx(self.c_r-1)));
+ }
+ self.c_r += 1;
+ }
+ self.c_l += 1;
+ self.c_r = 0;
+ }
+ return Option::None;
+ }
}
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/DeclarationGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/DeclarationGenerator.java
index 390145021fb112766500d7ef4127ebc44e47c2eb..3f10e23e83b04828a2645f8c0cdafb2898e61ba5 100644
--- a/src/main/java/de/hhu/stups/codegenerator/generators/DeclarationGenerator.java
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/DeclarationGenerator.java
@@ -289,6 +289,7 @@ public class DeclarationGenerator {
else if (def.getSetType() instanceof EnumeratedSetElementType) return ""; //TODO?
else if (def.getSetType() instanceof DeferredSetElementType) return ""; //TODO?
else if (def.getSetType() instanceof IntegerType) return ""; //TODO?
+ else if (def.getSetType() instanceof BoolType) return ""; //TODO?
else return generateSetDefinition(def);
}).collect(Collectors.toList());
}
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
index 5eba60827ead169c553a737389592fd87fb0e701..b5efb4b26b18334d7b6db31aab8868a658a387c0 100755
--- a/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
@@ -377,6 +377,7 @@ public class MachineGenerator implements AbstractVisitor<String, Void> {
private String generateCopyConstructor(MachineNode node) {
if((forModelChecking && !isIncludedMachine) || forVisualisation) {
ST template = currentGroup.getInstanceOf("copy_constructor");
+ if (template.getAttributes() == null || template.getAttributes().isEmpty()) return template.render(); // rust does not need this and it produces issues on embedded code generation
TemplateHandler.add(template, "machine", nameHandler.handle(node.getName()));
List<DeclarationNode> parameters = new ArrayList<>(node.getConstants());
parameters.addAll(node.getVariables());
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/TypeGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/TypeGenerator.java
index 9412875a0c4629180c8d1bbdff83f3010c9412bb..a8e78803a3f645ff51231c22875a8070d6dcfd6e 100644
--- a/src/main/java/de/hhu/stups/codegenerator/generators/TypeGenerator.java
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/TypeGenerator.java
@@ -172,7 +172,8 @@ public class TypeGenerator {
if (!this.forEmbedded) return null;
SetDefinition existingDef = this.setDefinitions.getDefinition(type);
if (existingDef != null) {
- if (constant || !existingDef.isConstant()) return existingDef; //returns dynamic set if it exists, even if constant set is 'requested'. Caller needs to check for that. (we only keep const-definitions if there is no dynamic one)
+ if (constant || !existingDef.isConstant())
+ return existingDef; //returns dynamic set if it exists, even if constant set is 'requested'. Caller needs to check for that. (we only keep const-definitions if there is no dynamic one)
else this.setDefinitions.deleteDefinition(type); //dynamic set found after const-set -> overwrite
}
@@ -201,6 +202,9 @@ public class TypeGenerator {
name = "BInteger";
// The integer-set is hard-coded into the BType-library (since there isn't a good way of creating it dynamically with generated code)
// Nesting of integer-sets is not supported at all (but the generator won't stop this)
+ } else if(type instanceof BoolType) {
+ variants = getTypeVariants(type);
+ name = "BOOL";
} else {
throw new RuntimeException("cannot add setDef for type "+type);
}
diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg
index 557f430f536c6f542aa22835c9141fb6f5243612..09c33dbda296ce4edb883936d4cf6436c95ad5e0 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg
@@ -23,21 +23,44 @@ use btypes::binteger::BInt;
use btypes::binteger::set_BInteger;
use btypes::btuple::BTuple;
+<if(forModelChecking)>
+use std::env;
+use std::sync::atomic::{AtomicU64, Ordering};
+use std::sync::{Arc, mpsc, Mutex};
+use std::collections::{HashSet, LinkedList};
+use dashmap::DashSet;
+use threadpool::ThreadPool;
+use std::sync::mpsc::channel;
+use derivative::Derivative;
+use std::time::{Duration};
+<endif>
+
<includedMachines; separator="\n">
+<if(forModelChecking)>
+#[derive(Clone, Copy)]
+pub enum MC_TYPE { BFS, DFS, MIXED }
+<endif>
+
<structs; separator="\n\n">
<enums; separator="\n\n">
<setDefinitions; separator="\n\n">
-#[derive(Default, Debug)]
+<if(forModelChecking)>
+#[derive(Derivative)]
+#[derivative(Clone, Default, Debug, Hash, PartialEq, Eq)]
+<else>#[derive(Default, Debug)]<endif>
pub struct <machine> {
<if(declarations)>/*declarations*/<declarations; separator="\n"><endif>
<if(includes)>/*includes*/<includes; separator="\n"><endif>
<if(constants_declarations)>/*constant_declarations*/<constants_declarations; separator="\n"><endif>
<if(sets)>/*sets*/<sets; separator="\n"><endif>
+ <if(forModelChecking)>
+ <if(transitionCachesDeclaration)>#[derivative(Hash="ignore", PartialEq="ignore")]<endif>
+ <transitionCachesDeclaration; separator="\n#[derivative(Hash=\"ignore\", PartialEq=\"ignore\")]\n"><endif>
}
<hash_equal>
@@ -47,10 +70,59 @@ impl <machine> {
<if(getters)><\n><getters; separator="\n\n"><endif>
<if(operations)><\n><operations; separator="\n\n">
<endif>
+
+ <if(forModelChecking)>
+
+ <transitions; separator="\n\n">
+
+ <invariant; separator="\n\n">
+
+ <copy>
+
+ <modelcheck>
+
+ <endif>
}
<lambdaFunctions; separator="\n\n">
<addition>
+
+<if(forModelChecking)>
+fn main() {
+ let args: Vec\<String> = env::args().collect();
+ 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."); }
+
+ let is_caching = args.get(3).unwrap().parse::\<bool>().unwrap();
+ let mc_type = match args.get(1).unwrap().as_str() {
+ "mixed" => MC_TYPE::MIXED,
+ "bf" => MC_TYPE::BFS,
+ "df" => MC_TYPE::DFS,
+ _ => panic!("Input for strategy is wrong.")
+ };
+
+ let mut no_dead = false;
+ let mut no_inv = false;
+
+ if args.len() > 4 {
+ for arg in args.iter().skip(4) {
+ match arg.as_str() {
+ "-nodead" => no_dead = true,
+ "-noinv" => no_inv = true,
+ _ => {}
+ }
+ }
+ }
+
+ if threads == 1 {
+ <machine>::model_check_single_threaded(mc_type, is_caching, no_dead, no_inv);
+ } else {
+ <machine>::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead, no_inv);
+ }
+}
+<endif>
>>
import_type(type, useBigInteger) ::= <<
@@ -522,7 +594,7 @@ global_declaration(type, identifier) ::= <<
>>
transition_cache_declaration(type, identifier, operationHasParams) ::= <<
-_tr_cache_<identifier>: Option\<<if(operationHasParams)>BSet\<<type>\><else>bool<endif>\>,
+_tr_cache_<identifier>: Option\<<if(operationHasParams)>HashSet\<<type>\><else>bool<endif>\>,
>>
constant_declaration(type, identifier) ::= <<
@@ -1074,17 +1146,9 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, n
}
>>
-copy_constructor(machine, parameters, assignments) ::= <<
-public <machine>(<parameters; separator=", ">) {
- //copy_constructor
- <assignments; separator="\n">
-}
->>
+copy_constructor() ::= <<>>
-copy_assignment(variable) ::= <<
-//copy_assignment
-this.<variable> = <variable>;
->>
+copy_assignment() ::= <<>>
pre_assert(isModelChecking, isTopLevel, iterationConstruct, predicate, then) ::= <<
//pre_assert
@@ -1101,7 +1165,7 @@ if <predicate> {
>>
transition(noParameters, noPredicate, identifier, subType, operationName, predicate, hasCondition, conditionalPredicate, combination) ::= <<
-pub fn _tr_<operationName>(&mut self, is_caching: bool) -> <if(noParameters)>bool<else>BSet\<<subType>\><endif> {
+pub fn _tr_<operationName>(&mut self, is_caching: bool) -> <if(noParameters)>bool<else>HashSet\<<subType>\><endif> {
//transition
if !is_caching || self._tr_cache_<operationName>.is_none() {
<if(noParameters)>
@@ -1114,7 +1178,7 @@ pub fn _tr_<operationName>(&mut self, is_caching: bool) -> <if(noParameters)>boo
return __tmp__val__;
<endif>
<else>
- let mut <identifier>: BSet\<<subType>\> = BSet::new(vec![]);
+ let mut <identifier>: HashSet\<<subType>\> = HashSet::new();
<if(hasCondition)>
if <conditionalPredicate> {
<combination>
@@ -1159,10 +1223,10 @@ parameter_combination_predicate(otherIterationConstructs, set, element, emptyPre
//parameter_combination_predicate TODO: FASTER
<otherIterationConstructs>
<if(emptyPredicate)>
-<set> = <set>.union(&BSet::new(vec![<element>]));
+<set>.insert(<element>);
<else>
if <predicate> {
- <set> = <set>.union(&BSet::new(vec![<element>]));
+ <set>.insert(<element>);
}
<endif>
>>
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestMCBenchmarks.java b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestMCBenchmarks.java
new file mode 100644
index 0000000000000000000000000000000000000000..ef1961600efb4a13b529b006bba0907c73e6ae3b
--- /dev/null
+++ b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestMCBenchmarks.java
@@ -0,0 +1,57 @@
+package de.hhu.stups.codegenerator.rust_embedded;
+
+import org.junit.Ignore;
+import org.junit.Test;
+
+import java.io.IOException;
+import java.net.URISyntaxException;
+
+public class TestMCBenchmarks extends TestRSE {
+ public TestMCBenchmarks() throws URISyntaxException, IOException {}
+
+ @Test
+ public void testCanBusMC() throws Exception {
+ testRSEMC("CAN_BUS_tlc");
+ }
+
+ @Test
+ public void testCruiseControllerDeterministic_MC() throws Exception {
+ testRSEMC("Cruise_finite1_deterministic_MC");
+ }
+
+ @Test
+ public void testLandingGear_MC() throws Exception {
+ testRSEMC("landing_gear/LandingGear_R6");
+ }
+
+ @Test
+ public void testLift_MC() throws Exception {
+ testRSEMC("Lift_MC_Large");
+ }
+
+ @Test
+ public void testNotaV2_MC() throws Exception {
+ testRSEMC("nota_v2");
+ }
+
+ @Test
+ @Ignore
+ public void testQueens4_MC() throws Exception {
+ testRSEMC("QueensWithEvents_4");
+ }
+
+ @Test
+ public void testsort_m2_data1000_MC() throws Exception {
+ testRSEMC("sort_m2_data1000_MC");
+ }
+
+ @Test
+ public void testTrain1_Lukas_POR_v3() throws Exception {
+ testRSEMC("Train1_Lukas_POR_v3");
+ }
+
+ @Test
+ public void testTrain_1_beebook_deterministic_MC_POR_v2() throws Exception {
+ testRSEMC("Train_1_beebook_deterministic_MC_POR_v2");
+ }
+}
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRSE.java b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRSE.java
index 4db16b36b8f4e0eee6e20d6865ca64ca9b59feb4..e663523b57774366627e5d486772dc7825d861ce 100644
--- a/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRSE.java
+++ b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRSE.java
@@ -23,7 +23,9 @@ import static org.junit.Assert.*;
public class TestRSE {
final ClassLoader classLoader = this.getClass().getClassLoader();
final Path tomlPath = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust_embedded/bmachine/Cargo.toml"));
+ final Path tomlPath_MC = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust_embedded/bmachine_mc/Cargo.toml"));
final Path rustSrcPath = tomlPath.getParent().resolve(Paths.get("src/"));
+ final Path rustSrcPath_MC = tomlPath_MC.getParent().resolve(Paths.get("src/"));
final Runtime runtime = Runtime.getRuntime();
final Path testFileBasePath = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().resolve("resources/test/de/hhu/stups/codegenerator/");
@@ -31,30 +33,32 @@ public class TestRSE {
Files.createDirectories(rustSrcPath);
}
- public void cleanup() {
- File[] oldFiles = rustSrcPath.toFile().listFiles();
+ public void cleanup(boolean modelChecking) {
+ File[] oldFiles = (!modelChecking ? rustSrcPath : rustSrcPath_MC).toFile().listFiles();
if (oldFiles != null) Arrays.stream(oldFiles).forEach(File::delete);
}
public void generateTestFiles(String machineRelPath, boolean modelChecking, String addition) throws IOException {
- if (addition == null) addition = "DefaultAddition.strs";
- cleanup();
+ if (addition == null && !modelChecking) addition = "DefaultAddition.strs";
+ cleanup(modelChecking);
+ final Path usedPath = !modelChecking ? rustSrcPath : rustSrcPath_MC;
Path machinePath = testFileBasePath.resolve(machineRelPath + ".mch");
List<Path> rsFilePaths = TestHelper.generateCode(machinePath, GeneratorMode.RS, modelChecking, addition, true);
rsFilePaths.forEach(path -> {
- Path dest = rustSrcPath.resolve(Paths.get(path.toFile().getName()));
+ Path dest = usedPath.resolve(Paths.get(path.toFile().getName()));
path.toFile().renameTo(dest.toFile());
});
int i = machineRelPath.lastIndexOf('/');
- File mainPath = rustSrcPath.resolve(machineRelPath.substring(i+1) + ".rs").toFile();
- File newMainFile = rustSrcPath.resolve("main.rs").toFile();
+ File mainPath = usedPath.resolve(machineRelPath.substring(i+1) + ".rs").toFile();
+ File newMainFile = usedPath.resolve("main.rs").toFile();
mainPath.renameTo(newMainFile);
}
- public void compileTestFiles() throws IOException, InterruptedException {
- Process process = runtime.exec("cargo build --release --manifest-path " + tomlPath);
+ public void compileTestFiles(boolean forModelChecking) throws IOException, InterruptedException {
+ Path usedTomlPath = !forModelChecking ? tomlPath : tomlPath_MC;
+ Process process = runtime.exec("cargo build --release --manifest-path " + usedTomlPath);
TestHelper.writeInputToSystem(process.getErrorStream());
TestHelper.writeInputToOutput(process.getErrorStream(), process.getOutputStream());
process.waitFor();
@@ -69,7 +73,9 @@ public class TestRSE {
if (noDead) { progArgs += " -nodead"; }
if (noInv) { progArgs += " -noinv"; }
- Process executeProcess = runtime.exec("cargo run --release --manifest-path " + tomlPath + progArgs);
+ Path usedTomlPath = !modelChecking ? tomlPath : tomlPath_MC;
+
+ Process executeProcess = runtime.exec("cargo run --release --manifest-path " + usedTomlPath + progArgs);
executeProcess.waitFor();
String error = TestHelper.streamToString(executeProcess.getErrorStream());
@@ -98,22 +104,29 @@ public class TestRSE {
}
public void testRSE(String machineName, String addition) throws IOException, InterruptedException {
- boolean execute = addition != null;
- boolean modelChecking = false;
+ testRSE(machineName, addition, false);
+ }
+
+ public void testRSEMC(String machineName) throws IOException, InterruptedException {
+ testRSE(machineName, null, true);
+ }
+
+ public void testRSE(String machineName, String addition, boolean modelChecking) throws IOException, InterruptedException {
+ boolean execute = modelChecking || addition != null;
boolean noInv = false;
boolean noDead = false;
generateTestFiles(machineName, modelChecking, addition);
- compileTestFiles();
+ compileTestFiles(modelChecking);
if(!execute) {
- cleanup();
+ cleanup(modelChecking);
return;
}
String result = runTestFiles(modelChecking, noDead, noInv);
verifyOutput(machineName, modelChecking, result);
- cleanup();
+ cleanup(modelChecking);
}
}