rust template and bboolean adjustments

fixed single-threaded modelchecking
fixed template errors regarding boolean-operations
simplified BBolean implementation

btypes_primitives/src/main/rust/bmachine/Cargo.toml

@@ -10,6 +10,7 @@ rand = "0.8.3"
 im = "15.0.0"
 threadpool = "1.8.1"
 derivative = "2.2.0"
+dashmap = "5.1.0"
 btypes = { path = "../btypes" }
 
 [profile.release]

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

-use std::hash::Hash;
 use crate::bobject::BObject;
-use std::fmt;
+
+pub type BBoolean = bool;
 
 pub trait IntoBool {
     #![allow(non_snake_case)]
     fn booleanValue(&self) -> bool;
 }
 
-impl IntoBool for bool {
-    fn booleanValue(&self) -> bool {
-        return *self;
-    }
-}
-
-#[derive(Default, Debug, Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
-pub struct BBoolean {
-    val: bool,
-}
-
-impl fmt::Display for BBoolean {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "{}", self.val)
-    }
+pub trait BBooleanT: BObject + IntoBool + Copy {
+    fn new(val: bool) -> Self;
+    fn or(&self, other: &Self) -> Self;
+    fn xor(&self, other: &Self) -> Self;
+    fn and(&self, other: &Self) -> Self;
+    fn not(&self) -> Self;
+    fn implies(&self, other: &Self) -> Self;
+    fn equivalent(&self, other: &Self) -> Self;
+    fn equal(&self, other: &Self) -> Self;
+    fn unequal(&self, other: &Self) -> Self;
 }
 
-impl BObject for BBoolean {}
-
-impl IntoBool for BBoolean {
+impl IntoBool for bool {
     fn booleanValue(&self) -> bool {
-        return self.val;
-    }
-}
-
-impl BBoolean {
-    #![allow(non_snake_case, dead_code)]
-
-    pub const fn new(v: bool) -> BBoolean {
-        return BBoolean {
-            val: v,
-        }
-    }
-
-    pub fn or(&self, other: &BBoolean) -> BBoolean {
-        return BBoolean::new(self.val || other.val);
-    }
-
-    pub fn xor(&self, other: &BBoolean) -> BBoolean {
-        return BBoolean::new(self.val ^ other.val);
-    }
-
-    pub fn and(&self, other: &BBoolean) -> BBoolean {
-        return BBoolean::new(self.val && other.val);
-    }
-
-    pub fn not(&self) -> BBoolean {
-        return BBoolean::new(!self.val);
+        return *self;
     }
-
-    pub fn implies(&self, other: &BBoolean) -> BBoolean {
-        return BBoolean::new(!self.val || other.val);
 }
 
-    pub fn equivalent(&self, other: &BBoolean) -> BBoolean {
-        return BBoolean::new(self.val == other.val);
-    }
+impl BObject for bool {}
 
-    pub fn equal(&self, other: &BBoolean) -> BBoolean {
-        return BBoolean::new(self.val == other.val);
-    }
-
-    pub fn unequal(&self, other: &BBoolean) -> BBoolean {
-        return BBoolean::new(self.val != other.val);
-    }
+impl BBooleanT for bool {
+    fn new(val: bool) -> Self { val }
+    fn or(&self, other: &Self) -> Self { *self || *other }
+    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 equivalent(&self, other: &Self) -> Self { *self == *other }
+    fn equal(&self, other: &Self) -> Self { *self == *other }
+    fn unequal(&self, other: &Self) -> Self { *self != *other }
 }

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

 use std::convert::TryInto;
-use crate::bboolean::BBoolean;
+use crate::bboolean::{BBoolean, BBooleanT};
 use crate::bobject::BObject;
 
 use std::fmt;

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

 use std::hash::Hash;
 use std::clone::Clone;
 use std::fmt::Display;
-use crate::bboolean::BBoolean;
+use crate::bboolean::{BBoolean, BBooleanT};
 
 pub trait BObject: Eq + Hash + Ord + Clone + Display {
     fn is_struct(&self) -> BBoolean { BBoolean::new(false) }

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

@@ -13,7 +13,7 @@ use std::convert::TryInto;
 use rand::prelude::IteratorRandom;
 use crate::orderedhashset::OrderedHashSet as OrdSet; //TODO try OrdMap instead
 use im::OrdMap as HashMap;
-use crate::bboolean::BBoolean;
+use crate::bboolean::{BBoolean, BBooleanT};
 use crate::brelation::CombiningType::{DIFFERENCE, INTERSECTION, UNION};
 use crate::bset::{BSet, SetLike, TBSet};
 use crate::bstring::TBString;

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

 #![ allow( dead_code, non_snake_case) ]
 
-use crate::bboolean::{IntoBool, BBoolean};
+use crate::bboolean::{IntoBool, BBoolean, BBooleanT};
 use crate::binteger::{BInt, BInteger};
 use crate::bstring::BString;
 use crate::bobject::BObject;

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

-use crate::bboolean::BBoolean;
+use crate::bboolean::{BBoolean, BBooleanT};
 use crate::bobject::BObject;
 
 pub trait BStruct: BObject{

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

-use crate::bboolean::BBoolean;
+use crate::bboolean::{BBoolean, BBooleanT};
 use crate::bset::BSet;
 
 lazy_static! {

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

@@ -4,21 +4,22 @@ as, break, const, continue, crate, else, enum, extern, false, fn, for, if, impl,
 
 
 machine(imports, includedMachines, machine, structs, constants_declarations, includes, enums, sets, declarations, initialization, operations, addition, useBigInteger, getters, lambdaFunctions, forModelChecking, transitions, invariant, copy, modelcheck, transitionCachesDeclaration) ::= <<
-#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
+#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
 <if(forModelChecking)>
 use std::env;
 use std::sync::atomic::{AtomicU64, Ordering};
-use std::sync::{Arc, Mutex};
+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>
 use std::fmt;
 use rand::{thread_rng, Rng};
 use btypes::butils;
-use btypes::bboolean::IntoBool;
+use btypes::bboolean::{IntoBool, BBooleanT};
 <imports; separator="\n">
 <includedMachines; separator="\n">
 
@@ -83,11 +84,11 @@ fn main() {
         _    => panic!("Input for strategy is wrong.")
     };
 
-    //TODO: if threads == 1 {
-    //    <machine>::model_check_single_threaded(mc_type, is_caching);
-    //} else {
+    if threads == 1 {
+        <machine>::model_check_single_threaded(mc_type, is_caching);
+    } else {
         <machine>::modelCheckMultiThreaded(mc_type, threads, is_caching);
-    //}
+    }
 }
 <endif>
 >>
@@ -187,7 +188,8 @@ impl <name> {
 
     <functions; separator="\n\n">
 
-    pub fn equal(&self, other: &<name>) -> BBoolean {
+    pub fn equal(
+    &self, other: &<name>) -> BBoolean {
         return BBoolean::new(<equalPredicates; separator=" && ">);
     }
 
@@ -533,11 +535,11 @@ binary(arg1,operator,arg2) ::= <<
 >>
 
 or(arg1, arg2) ::= <<
-<arg1>.booleanValue() || <arg2>.booleanValue()
+(<arg1> || <arg2>)
 >>
 
 and(arg1, arg2) ::= <<
-<arg1>.booleanValue() && <arg2>.booleanValue()
+(<arg1> && <arg2>)
 >>
 
 implies(arg1, arg2) ::= <<
@@ -769,9 +771,10 @@ fn generateNextStates(state: &mut <machine>,
                       isCaching: bool,
                       transitions: Arc\<AtomicU64>) -> HashSet\<(<machine>, &'static str)> {
     let mut result = HashSet::\<(<machine>, &'static str)>::new();
+    let mut evaluated_transitions: u64 = 0;
     <transitionsWithCaching>
 
-    transitions.fetch_add(result.len() as u64, Ordering::AcqRel);
+    transitions.fetch_add(evaluated_transitions, Ordering::AcqRel);
     return result;
 }
 >>
@@ -779,18 +782,11 @@ fn generateNextStates(state: &mut <machine>,
 model_check_transition(hasParameters, tupleType, transitionIdentifier, evalTransitions, execTransitions, isCaching) ::= <<
 //model_check_transition
 <if(hasParameters)>
-<if(isCaching)>
 let mut <transitionIdentifier> = state.<evalTransitions>(isCaching);
 for param in <transitionIdentifier>.iter().cloned() {
     <execTransitions>
 }
 <else>
-let mut <transitionIdentifier> = state.<evalTransitions>(isCaching);
-for param in <transitionIdentifier>.iter().cloned() {
-    <execTransitions>
-}
-<endif>
-<else>
 if state.<evalTransitions>(isCaching) {
     <execTransitions>
 }
@@ -827,6 +823,7 @@ let mut copiedState = state.clone();
 copiedState.<operation>(<parameters; separator=", ">);
 if isCaching { copiedState.invalidate_caches(Self::get_guard_dependencies("<operation>")); }
 result.insert((copiedState, "<operation>"));
+evaluated_transitions += 1;
 >>
 
 model_check_transition_param_assignment(type, param, val, isLhs, oneParameter) ::= <<
@@ -889,68 +886,47 @@ fn get_invariant_dependencies(op: &'static str) -> Vec\<&str> {
         _ => vec![],
     }
 }
-/*
+
 fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool) {
     let mut machine = <machine>::new();
 
-    let invariant_violated = AtomicBool::new(false);
-    let deadlock_detected = AtomicBool::new(false);
-    let stop_threads = AtomicBool::new(false);
-
-    if <invariants:{inv | !machine.<inv>()}; separator=" || "> {
-        invariant_violated.store(true, Ordering::Release);
-    }
-
-    let mut states = HashSet::\<<machine>\>::new();
-    states.insert(machine.clone());
-
-    let collection_m = Arc::new(Mutex::new(LinkedList::\<<machine>\>::new()));
-    collection_m.lock().unwrap().push_back(machine.clone());
+    let mut all_states = HashSet::\<<machine>\>::new();
+    all_states.insert(machine.clone());
 
-    let mut invariantDependency = HashMap::\<&str, HashSet\<&'static str>\>::new();
-    let mut guardDependency = HashMap::\<&str, HashSet\<&'static str>\>::new();
-    let mut dependent_invariant_m = Arc::new(Mutex::new(HashMap::\<<machine>, HashSet\<&str>\>::new()));
+    let states_to_process_mutex = Arc::new(Mutex::new(LinkedList::\<(<machine>, &'static str)>::new()));
+    states_to_process_mutex.lock().unwrap().push_back((machine.clone(), ""));
 
-    if is_caching {
-        <invariantDependency; separator="\n">
-        <guardDependency; separator="\n">
-        dependent_invariant_m.lock().unwrap().insert(machine.clone(), HashSet::new());
-    }
+    let num_transitions = Arc::new(AtomicU64::new(0));
 
-    let transitions = Arc::new(AtomicU64::new(0));
+    let mut stop_threads = false;
 
-    while !stop_threads.load(Ordering::Acquire) && !collection_m.lock().unwrap().is_empty() {
-        let mut state = Self::next(Arc::clone(&collection_m), mc_type);
+    while !stop_threads && !states_to_process_mutex.lock().unwrap().is_empty() {
+        let (mut state, last_op) = Self::next(Arc::clone(&states_to_process_mutex), mc_type);
 
-        let next_states = Self::generateNextStates(&mut state, is_caching, &mut invariantDependency, Arc::clone(&dependent_invariant_m), &mut guardDependency, Arc::clone(&transitions));
+        let next_states = Self::generateNextStates(&mut state, is_caching, Arc::clone(&num_transitions));
 
-        next_states.iter().cloned().for_each(|next_state| {
-            if !states.contains(&next_state) {
-                states.insert(next_state.clone());
-                let cnum_states = states.len();
-                collection_m.lock().unwrap().push_back(next_state);
-                if cnum_states % 50000 == 0 {
-                    println!("VISITED STATES: {}", cnum_states);
-                    println!("EVALUATED TRANSITIONS: {}", transitions.load(Ordering::Acquire));
-                    println!("-------------------");
-                }
+        if !Self::checkInvariants(&state, last_op, is_caching) {
+            println!("INVARIANT VIOLATED");
+            stop_threads = true;
         }
-        });
-
         if next_states.is_empty() {
-            deadlock_detected.store(true, Ordering::Release);
-            stop_threads.store(true, Ordering::Release);
+            print!("DEADLOCK DETECTED");
+            stop_threads = true;
         }
 
-        if !Self::checkInvariants(&state, is_caching, Arc::clone(&dependent_invariant_m)) {
-            invariant_violated.store(true, Ordering::Release);
-            stop_threads.store(true, Ordering::Release);
-        }
+        next_states.into_iter()
+                   .filter(|(next_state, _)| all_states.insert((*next_state).clone()))
+                   .for_each(|(next_state, last_op)| states_to_process_mutex.lock().unwrap().push_back((next_state, last_op)));
 
+        if all_states.len() % 50000 == 0 {
+            println!("VISITED STATES: {}", all_states.len());
+            println!("EVALUATED TRANSITIONS: {}", num_transitions.load(Ordering::Acquire));
+            println!("-------------------");
+        }
     }
-    Self::print_result(states.len(), transitions.load(Ordering::Acquire), deadlock_detected.load(Ordering::Acquire), invariant_violated.load(Ordering::Acquire));
+    Self::print_result(all_states.len(), num_transitions.load(Ordering::Acquire), stop_threads);
 }
-*/
+
 fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
     let threadPool = ThreadPool::new(threads);
 
@@ -980,11 +956,11 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
         //println!("Thread {:?} spawning a thread", thread::current().id());
         threadPool.execute(move|| {
             if !Self::checkInvariants(&state, last_op, is_caching) {
-                tx.send(Err("INVARIANT VIOLATED")).expect("");
+                let _ = tx.send(Err("INVARIANT VIOLATED"));
             }
 
             let next_states = Self::generateNextStates(&mut state, is_caching, transitions);
-            if next_states.is_empty() { tx.send(Err("DEADLOCK DETECTED")).expect(""); }
+            if next_states.is_empty() { let _ = tx.send(Err("DEADLOCK DETECTED")); }
 
             //println!("Thread {:?} executing", thread::current().id());
             next_states.into_iter()
@@ -992,7 +968,7 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
                        .for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
 
             //println!("Thread {:?} done", thread::current().id());
-            tx.send(Ok(1)).expect("");
+            let _ = tx.send(Ok(1));
         });
 
         spawned_tasks += 1;
@@ -1004,10 +980,14 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool) {
 
         while states_to_process_mutex.lock().unwrap().is_empty() && spawned_tasks - finished_tasks > 0 {
             //println!("Thread {:?} (main) waiting for a thread to finish", thread::current().id());
-            match rx.recv() {
+            match rx.recv_timeout(Duration::from_secs(1)) {
+                Ok(val)  => match val {
                         Ok(_) => finished_tasks += 1,
-                Err(_) => stop_threads = true,
+                        Err(msg) => { println!("{}", msg); stop_threads = true; },
+                    },
+                Err(_) => (),
             }
+            if threadPool.panic_count() > 0 { stop_threads = true; }
         }
     }