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 0f5c09b7dddc304ac6cbb14a31bd95ac840d14bb..ee58642cf563ba8ace53ce085f2ed0d0a99ce06a 100644 --- a/btypes_primitives/src/main/rust_embedded/btypes/src/binteger.rs +++ b/btypes_primitives/src/main/rust_embedded/btypes/src/binteger.rs @@ -1,11 +1,49 @@ +#![allow(non_snake_case)] +use core::convert::TryInto; pub type BInteger = i128; pub trait BInt { - fn equal(&self, other: Self) -> bool; + fn equal(&self, other: &Self) -> bool; + + fn greater(&self, other: &Self) -> bool; + fn greaterEqual(&self, other: &Self) -> bool; + fn less(&self, other: &Self) -> bool; + fn lessEqual(&self, other: &Self) -> bool; + + fn plus(&self, other: &Self) -> Self; + fn minus(&self, other: &Self) -> Self; + fn multiply(&self, other: &Self) -> Self; + fn divide(&self, other: &Self) -> Self; + fn modulo(&self, other: &Self) -> Self; + fn power(&self, exp: &Self) -> Self; + + fn negative(&self) -> Self; + fn pred(&self) -> Self; + fn succ(&self) -> Self; } impl BInt for BInteger { - fn equal(&self, other: Self) -> bool { self.eq(&other) } + fn equal(&self, other: &Self) -> bool { self.eq(&other) } + + fn greater(&self, other: &Self) -> bool { self > other } + fn greaterEqual(&self, other: &Self) -> bool { self >= other } + fn less(&self, other: &Self) -> bool { self < other } + fn lessEqual(&self, other: &Self) -> bool { self <= other } + + fn plus(&self, other: &Self) -> Self { self + other } + fn minus(&self, other: &Self) -> Self { self - other } + fn multiply(&self, other: &Self) -> Self { self * other } + fn divide(&self, other: &Self) -> Self { self / other } + fn modulo(&self, other: &Self) -> Self { self % other } + fn power(&self, exp: &Self) -> Self { + if exp < &0 { panic!("Power with negative exponent!") } + let u32_exp: u32 = exp.unsigned_abs().try_into().unwrap(); + return self.pow(u32_exp); + } + + fn negative(&self) -> Self { -self } + fn pred(&self) -> Self { self - 1 } + fn succ(&self) -> Self { self + 1 } } \ No newline at end of file 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 2d418f2ad96754443bb2ff70326986e24d0b274d..c8e15220d577f9b1a66a7b34ae6acc0ef6f1b601 100644 --- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg +++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg @@ -5,15 +5,17 @@ as, break, const, continue, crate, else, enum, extern, false, fn, for, if, impl, machine(imports, includedMachines, machine, structs, constants_declarations, includes, enums, sets, setDefinitions, declarations, initialization, operations, addition, useBigInteger, getters, lambdaFunctions, forModelChecking, transitions, invariant, copy, modelcheck, transitionCachesDeclaration, hash_equal) ::= << #![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ] +//#![no_std] //std is enabled for the generated machine by default, since without it there is no println which makes unit-testing very difficult use btypes::{bset, brel}; -//use btypes::set::{BSet, SetItem, BRelation, RelItem}; use btypes::bset::BSet; use btypes::bset::SetItem; use btypes::bset::PowSetItem; use btypes::brelation::BRelation; use btypes::brelation::RelLeftItem; use btypes::bboolean::BBoolean; +use btypes::bboolean::BBool; use btypes::binteger::BInteger; +use btypes::binteger::BInt; <includedMachines; separator="\n">