updated Java-MC benchmark files

also fixed some issues in the readme and added rust as an option to the base makefile

Makefile

@@ -7,6 +7,7 @@ JAVA_DEPENDENCIES= :btypes.jar
 CPP_CODE_GEN_FLAGS=-l cpp -mc true
 CPPC ?= clang++
 CPPFLAGS ?= -std=c++14 -O1 -flto
+RS_CODE_GEN_FLAGS=-l rs -mc true
 STRATEGY=mixed
 THREADS=1
 CACHING=false
@@ -42,6 +43,13 @@ ifeq ($(LANGUAGE), cpp)
 	$(CPPC) $(CPPFLAGS) -o $@.exec $@.cpp
 	./$@.exec $(STRATEGY) $(THREADS) $(CACHING)
 endif
+ifneq (,$(findstring $(LANGUAGE), rs|RS|rust|Rust))
+%:
+	java -jar B2Program-all-0.1.0-SNAPSHOT.jar $(RS_CODE_GEN_FLAGS) -f $(DIRECTORY)/$@.mch
+	mv $(DIRECTORY)/$@.rs ./btypes_primitives/src/main/rust/bmachine/src/main.rs
+	mv $(DIRECTORY)/*.rs ./btypes_primitives/src/main/rust/bmachine/src/
+	cargo run --release --manifest-path ./btypes_primitives/src/main/rust/bmachine/Cargo.toml -- $(STRATEGY) $(THREADS) $(CACHING)
+endif
 endif
 
 # Usage:

README.md

@@ -122,7 +122,7 @@ P is a conjunction of n conjuncts where the i-th conjunct must constraint xi for
 | Predicate             | Meaning    |
 |-----------------------|------------|
 | E = F                 | equality   |
-| E \= F                | inequality |
+| E \\= F               | inequality |
 
 ### Booleans:
 
@@ -141,7 +141,7 @@ P is a conjunction of n conjuncts where the i-th conjunct must constraint xi for
 | {}                            | Empty Set                                  |
 | {E}                           | Singleton Set                              |
 | {E,F,...}                     | Set Enumeration                            |
-| {x1,...,xn\                   |P}               | Set Comprehension                          |
+| {x1,...,xn|P}            | Set Comprehension                          |
 | POW(S)                        | Power Set                                  |
 | POW1(S)                       | Set of Non-Empty Subsets                   |
 | FIN(S)                        | Set of All Finite Subsets                  |
@@ -235,7 +235,7 @@ Restriction: Set of Relation mostly grows up very fast. They are only supported
 ### Functions:
 
 | Function Expression      | Meaning                           |
-|---------------------|-----------------------------------|
+|--------------------------|-----------------------------------|
 | S +-> T                  | Partial Function                  |
 | S --> T                  | Total Function                    |
 | S +->> T                 | Partial Surjection                |
@@ -243,7 +243,7 @@ Restriction: Set of Relation mostly grows up very fast. They are only supported
 | S >+> T                  | Partial Injection                 |
 | S >+>> T                 | Partial Bijection                 |
 | S >->> T                 | Total Bijection                   |
-| %(x1,...,xn).(P\|E) | Lambda Abstraction                |
+| %(x1,...,xn).(P|E)  | Lambda Abstraction                |
 | f(E)                     | Function Application              |
 | f(E1,...,EN)             | Function Application with Couples |
 

benchmarks/average_benchmark_results.py

+import statistics
+import sys
+from datetime import timedelta
+
+file = sys.argv[1]
+print('opening file: ', file)
+
+#      {machine: { (mode: str, threads: int, caching: bool): {times: [], memory: []} }}
+data = {}
+
+with open(file, 'r') as lines:
+    for line in lines:
+        #print('parsing line: ', line)
+        stripped_line = line.strip()
+        if stripped_line == '' or stripped_line.startswith('-'):
+            continue
+        machine, mode, threads, caching, time, memory = stripped_line.split(' ')
+        if machine not in data:
+            data[machine] = {}
+        params = (mode, int(threads), caching == 'true')
+        if params not in data[machine]:
+            data[machine][params] = {'times': [], 'memory': []}
+        data[machine][params]['times'] += [time]
+        data[machine][params]['memory'] += [int(memory)]
+
+for machine in data.keys():
+    for params in data[machine]:
+        times = data[machine][params]['times']
+        avg_time = timedelta()
+        number_of_datapoints = 0
+
+        for time in times:
+            number_of_datapoints += 1
+            minutes = 0
+            if ':' in time:
+                split = time.split(':')
+                minutes = int(split[0])
+                time = split[1]
+
+            millis = 0
+            if '.' in time:
+                split = time.split('.')
+                millis = int(split[1].ljust(3, '0'))
+                time = split[0]
+
+            seconds = int(time)
+            avg_time += timedelta(minutes=minutes, seconds=seconds, milliseconds=millis)
+        if number_of_datapoints > 0:
+            avg_time /= number_of_datapoints
+
+        memories = data[machine][params]['memory']
+
+        print(f'{machine} {params[0]} {params[1]} {params[2]} {round(avg_time.total_seconds(), 2)} {round(statistics.fmean(memories))}')

benchmarks/model_checking/Java/Cruise_finite1_deterministic_MC.java

@@ -12,6 +12,7 @@ import java.util.Map;
 import java.util.Set;
 import java.util.concurrent.atomic.AtomicBoolean;
 import java.util.concurrent.atomic.AtomicInteger;
+import java.util.concurrent.ConcurrentHashMap;
 import java.util.concurrent.ThreadPoolExecutor;
 import java.util.concurrent.Future;
 import java.util.concurrent.Executors;
@@ -813,7 +814,7 @@ public class Cruise_finite1_deterministic_MC {
         private final boolean isDebug;
 
         private final LinkedList<Cruise_finite1_deterministic_MC> unvisitedStates = new LinkedList<>();
-        private final Set<Cruise_finite1_deterministic_MC> states = new HashSet<>();
+        private final Set<Cruise_finite1_deterministic_MC> states = ConcurrentHashMap.newKeySet();
         private AtomicInteger transitions = new AtomicInteger(0);
         private ThreadPoolExecutor threadPool;
         private Object waitLock = new Object();
@@ -906,9 +907,7 @@ public class Cruise_finite1_deterministic_MC {
                     Set<Cruise_finite1_deterministic_MC> nextStates = generateNextStates(state);
 
                     nextStates.forEach(nextState -> {
-                        synchronized (states) {
-                            if(!states.contains(nextState)) {
-                                states.add(nextState);
+                        if(states.add(nextState)) {
                             synchronized (unvisitedStates) {
                                 unvisitedStates.add(nextState);
                             }
@@ -918,7 +917,6 @@ public class Cruise_finite1_deterministic_MC {
                                 System.out.println("-------------------");
                             }
                         }
-                        }
                     });
 
                     synchronized (unvisitedStates) {

benchmarks/model_checking/Java/Lift_MC_Large.java

@@ -10,6 +10,7 @@ import java.util.Map;
 import java.util.Set;
 import java.util.concurrent.atomic.AtomicBoolean;
 import java.util.concurrent.atomic.AtomicInteger;
+import java.util.concurrent.ConcurrentHashMap;
 import java.util.concurrent.ThreadPoolExecutor;
 import java.util.concurrent.Future;
 import java.util.concurrent.Executors;
@@ -141,7 +142,7 @@ public class Lift_MC_Large {
         private final boolean isDebug;
 
         private final LinkedList<Lift_MC_Large> unvisitedStates = new LinkedList<>();
-        private final Set<Lift_MC_Large> states = new HashSet<>();
+        private final Set<Lift_MC_Large> states = ConcurrentHashMap.newKeySet();
         private AtomicInteger transitions = new AtomicInteger(0);
         private ThreadPoolExecutor threadPool;
         private Object waitLock = new Object();
@@ -234,9 +235,7 @@ public class Lift_MC_Large {
                     Set<Lift_MC_Large> nextStates = generateNextStates(state);
 
                     nextStates.forEach(nextState -> {
-                        synchronized (states) {
-                            if(!states.contains(nextState)) {
-                                states.add(nextState);
+                        if(states.add(nextState)) {
                             synchronized (unvisitedStates) {
                                 unvisitedStates.add(nextState);
                             }
@@ -246,7 +245,6 @@ public class Lift_MC_Large {
                                 System.out.println("-------------------");
                             }
                         }
-                        }
                     });
 
                     synchronized (unvisitedStates) {

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

@@ -20,6 +20,8 @@ impl Display for BString {
 impl BObject for BString {}
 
 impl BString {
+    #![allow(non_snake_case, dead_code)]
+
     pub fn new(init: &str) -> BString {
         return BString { val: String::from(init) }
     }

src/main/java/de/hhu/stups/codegenerator/CodeGenerator.java

@@ -7,7 +7,6 @@ import de.hhu.stups.codegenerator.generators.CodeGenerationException;
 import de.hhu.stups.codegenerator.generators.MachineGenerator;
 import de.hhu.stups.codegenerator.generators.MachineReferenceGenerator;
 import de.hhu.stups.codegenerator.generators.VisualisationGenerator;
-import de.hhu.stups.codegenerator.json.JSONASTBuilder;
 import de.hhu.stups.codegenerator.json.modelchecker.ModelCheckingInfo;
 import de.hhu.stups.codegenerator.json.simb.SimulationRewriter;
 import de.hhu.stups.codegenerator.json.visb.VisBFileHandler;
@@ -114,6 +113,7 @@ public class CodeGenerator {
 			DefaultParser parser = new DefaultParser();
 			return parser.parse(options, args);
 		} catch (ParseException e) {
+			System.out.println(e.getMessage());
 			new HelpFormatter().printHelp("{-l <language> -bi <use_big_integer> -min <minint> -max <maxint> -dss <deferred_set_size> -cs <use_constraint_solving> -mc <forModelChecking> -f <filename> -v <visualisation> -a <additionalMain>} | -sim <simb_file>", options);
 		}
 		return null;
@@ -142,7 +142,7 @@ public class CodeGenerator {
 		} else if("rs".equals(languageOption)) {
 			mode = GeneratorMode.RS;
 		} else {
-			throw new RuntimeException("Wrong argument for language (must be java, python, c, cpp, clojure, ts)");
+			throw new RuntimeException(String.format("Wrong argument '%s' for language (must be java, python, c, cpp, clojure, ts, rs)", languageOption));
 		}
 		return mode;
 	}