added sequence support

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

@@ -29,6 +29,8 @@ pub trait BInt {
     fn negative(&self) -> Self;
     fn pred(&self) -> Self;
     fn succ(&self) -> Self;
+
+    fn from(source: BInteger) -> Self;
 }
 
 impl BInt for BInteger {
@@ -54,6 +56,8 @@ impl BInt for BInteger {
     fn negative(&self) -> Self { -self }
     fn pred(&self) -> Self { self - 1 }
     fn succ(&self) -> Self { self + 1 }
+
+    fn from(source: BInteger) -> Self { source }
 }
 
 

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

@@ -2,7 +2,7 @@
 
 use core::marker::PhantomData;
 use crate::bboolean::BBoolean;
-use crate::binteger::BInteger;
+use crate::binteger::{BInt, BInteger};
 use crate::bset::{BSet, PowSetItem, Set, SetItem};
 
 #[derive(Debug, Clone, Eq, PartialEq, Hash, PartialOrd, Ord)]
@@ -56,10 +56,55 @@ where L: SetItem<LS> + RelLeftItem<LS, R, RS, SIZE, REL_SIZE>,
         return BRelation { rel: L::idx_to_rel(idx), _p: PhantomData, _p2: PhantomData };
     }
 }
+/*
+impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> Set<REL_SIZE> for BRelation<L, LS, R, RS, REL_SIZE>
+    where L: SetItem<LS> + RelLeftItem<LS, R, RS, REL_SIZE>,
+          R: SetItem<RS>{
+    type ItemType = L::RelEnum;
+
+    fn as_arr(&self) -> [bool; REL_SIZE] {
+        todo!()
+    }
+
+    fn from_arr(arr: [bool; REL_SIZE]) -> Self {
+        todo!()
+    }
 
-//impl<I> PowAble<> for I
-//where I: SetItem<>
-//TODO: pow/fin/pow1/fin1, maybe
+    fn contains_idx(&self, idx: usize) -> bool {
+        todo!()
+    }
+
+    fn subset_of(&self, other: &Self) -> bool {
+        todo!()
+    }
+}
+*/
+
+pub trait RelPowAble<const REL_VARIANTS: usize, const REL_SIZE: usize>: SetItem<REL_VARIANTS> {
+    fn pow(&self) -> BSet<Self, REL_VARIANTS>;
+    fn pow1(&self) -> BSet<Self, REL_VARIANTS>;
+}
+
+impl<L, const LS: usize, R, const RS: usize, const SIZE: usize, const REL_SIZE: usize> RelPowAble<SIZE, REL_SIZE> for BRelation<L, LS, R, RS, REL_SIZE>
+    where L: SetItem<LS> + RelLeftItem<LS, R, RS, SIZE, REL_SIZE>,
+          R: SetItem<RS>{
+    fn pow(&self) -> BSet<Self, SIZE> {
+        let mut result_arr = [false; SIZE];
+        for idx in 0..SIZE {
+            let crel = Self::from_idx(idx);
+            result_arr[idx] = self.subset(&crel);
+        }
+        return BSet::<Self, SIZE>::const_from_arr(result_arr);
+    }
+
+    fn pow1(&self) -> BSet<Self, SIZE> {
+        let mut result_arr = self.pow().as_arr();
+        let empty_self = Self::empty();
+        let empty_idx = empty_self.as_idx();
+        result_arr[empty_idx] = false;
+        return BSet::const_from_arr(result_arr);
+    }
+}
 
 impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L, LS, R, RS, REL_SIZE>
     where L: SetItem<LS>,
@@ -300,6 +345,7 @@ impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L,
         return !self.rel[k.as_idx()][v.as_idx()];
     }
 
+    //subset or equal
     pub fn subset(&self, other: &Self) -> BBoolean {
         for left_idx in 0..LS {
             for right_idx in 0..RS {
@@ -403,6 +449,73 @@ where L: SetItem<LS> {
         return result;
     }
 }
+
+//Sequence
+impl<L, const LS: usize, R, const RS: usize, const REL_SIZE: usize> BRelation<L, LS, R, RS, REL_SIZE>
+where L: SetItem<LS> + BInt,
+      R: SetItem<RS>{
+
+    pub fn first(&self) -> R { self.functionCall(&L::from(1)) }
+    pub fn last(&self) -> R { self.functionCall(&L::from(self.card())) }
+    pub fn size(&self) -> BInteger { self.card() }
+
+    pub fn concat(&self, other: &Self) -> Self {
+        let mut result = self.copy();
+        let self_size = self.size();
+        for i in 1..=other.size() {
+            result.add_tuple(&L::from(self_size + i), &other.functionCall(&L::from(i)));
+        }
+        return result;
+    }
+
+    pub fn prepend(&self, e: &R) -> Self {
+        let mut result = Self::empty();
+        result.add_tuple(&L::from(1), e);
+        return result.concat(self);
+    }
+
+    pub fn append(&self, e: &R) -> Self {
+        let mut result = self.copy();
+        result.add_tuple(&L::from(self.size()+1), e);
+        return result;
+    }
+
+    pub fn reverse(&self) -> Self {
+        let mut result = Self::empty();
+        let self_size = self.size();
+        for i in 1..=self_size {
+            result.add_tuple(&L::from(i), &self.functionCall(&L::from(self_size - i + 1)))
+        }
+        return result;
+    }
+
+    pub fn front(&self) -> Self {
+        return self.take(&self.size().pred());
+    }
+
+    pub fn tail(&self) -> Self {
+        return self.drop(&1);
+    }
+
+    pub fn take(&self, n: &BInteger) -> Self {
+        let mut result = self.copy();
+        for i in (*n+1)..=self.size() {
+            let i_as_l = L::from(i);
+            result.rel[i_as_l.as_idx()][self.functionCall(&i_as_l).as_idx()] = false;
+        }
+        return result;
+    }
+
+    pub fn drop(&self, n: &BInteger) -> Self {
+        let mut result = Self::empty();
+        for i in (*n+1)..=self.size() {
+            result.add_tuple(&L::from(i-(*n)), &self.functionCall(&L::from(i)))
+        }
+        return result;
+    }
+}
+
+
 /* // Does not work in stable rust
 impl<L, const LS: usize, R, const RS: usize, const TOTAL: usize, const INNER_RS: usize> BRelation<L, LS, R, RS, TOTAL>
   where L: SetItem<LS>,

src/main/java/de/hhu/stups/codegenerator/generators/ExpressionGenerator.java

@@ -480,7 +480,7 @@ public class ExpressionGenerator {
         if (!this.forEmbedded) return;
         if (!(expr.getType() instanceof SetType)) return;
         BType subType = ((SetType) expr.getType()).getSubType();
-        SetDefinition setDef = typeGenerator.addSetDefinition(subType, true); //create const-setDef is necessary
+        SetDefinition setDef = typeGenerator.addSetDefinition(subType, true); //create const-setDef if necessary
         if (!setDef.isConstant()) return; //skip if a dynamic set of this type is already present
         if (expr instanceof ExpressionOperatorNode) {
             ExpressionOperatorNode opNode = (ExpressionOperatorNode) expr;
@@ -974,6 +974,7 @@ public class ExpressionGenerator {
         TemplateHandler.add(enumeration,"elements", tuples);
         TemplateHandler.add(enumeration, "type", typeGenerator.generate(rhsType));
         TemplateHandler.add(enumeration, "isParameter", isParameter);
+        TemplateHandler.add(enumeration, "relationName", declarationGenerator.generateSetEnumName(subType));
         return enumeration.render();
     }
 
@@ -981,24 +982,7 @@ public class ExpressionGenerator {
     * This function generates code for sequence enumeration from the given semantic information
     */
     private String generateSeqEnumeration(BType type, List<String> expressions) {
-        ST enumeration = currentGroup.getInstanceOf("seq_enumeration");
-        BType subType = ((SetType) type).getSubType();
-        BType rhsType = ((CoupleType) subType).getRight();
-        List<String> tuples = new ArrayList<>();
-        if(expressions.size() > 0) {
-            importGenerator.addImport(new CoupleType(new UntypedType(), new UntypedType()));
-        }
-        importGenerator.addImport(IntegerType.getInstance());
-        for(int i = 1; i <= expressions.size(); i++) {
-            ST number = currentGroup.getInstanceOf("number");
-            TemplateHandler.add(number, "number", String.valueOf(i));
-            TemplateHandler.add(number, "useBigInteger", useBigInteger);
-            String lhs = number.render();
-            tuples.add(generateTuple(Arrays.asList(lhs, expressions.get(i-1)), IntegerType.getInstance(), rhsType));
-        }
-        TemplateHandler.add(enumeration,"elements", tuples);
-        TemplateHandler.add(enumeration, "type", typeGenerator.generate(rhsType));
-        return enumeration.render();
+        return generateSeqEnumeration(type, expressions, false);
     }
 
     /*

src/main/java/de/hhu/stups/codegenerator/generators/TypeGenerator.java

@@ -163,6 +163,7 @@ public class TypeGenerator {
         TemplateHandler.add(template, "rightType", generate(type.getRight(), constant));
         addSetDefinition(type.getRight(), constant);
         TemplateHandler.add(template, "rightName", declarationGenerator.generateSetEnumName(type.getRight()));
+        addSetDefinition(type, constant);
         return template.render();
     }
 

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

@@ -14,6 +14,7 @@ use btypes::bset::PowAble;
 use btypes::bset::NestedSet;
 use btypes::brelation::BRelation;
 use btypes::brelation::RelLeftItem;
+use btypes::brelation::RelPowAble;
 use btypes::bboolean::BBoolean;
 use btypes::bboolean::BBool;
 use btypes::bboolean::BOOL;
@@ -374,7 +375,8 @@ set_enumeration(leftType, type, rightType, relationName, enums, isRelation) ::=
 <else>bset![<type><if(enums)>, <endif><enums; separator=", ">]<endif>
 >>
 
-seq_enumeration(type, elements) ::= <<
+seq_enumeration(type, elements, relationName) ::= <<
+<set_enumeration(leftType="BInteger", rightType=type, relationName=relationName, enums=elements, isRelation=true)>
 /*seq_enumeration <type>; <elements; separator=", "> */
 >>
 

src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestBenchmarks.java

@@ -38,7 +38,15 @@ public class TestBenchmarks extends TestRSE {
         testRSE("setoperationbenchmarks/SetOperation",  "SetOperationAddition.strs");
     }
 
-    //TODO: CAN_BUS: either allow const-intSet or rewrite machine
+    @Test
+    public void testCAN_BUS_tcl() throws Exception {
+        testRSE("CAN_BUS_tlc_exec", "CAN_BUS_tlc_execAddition.strs");
+    }
+
+    @Test
+    public void testCAN_BUS_NOIntSet() throws Exception {
+        testRSE("embedded/CAN_BUS_tlc_exec", "CAN_BUS_tlc_execAddition.strs");
+    }
 
     @Test
     public void testCruise_finite_deterministic() throws Exception {

src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestRelation.java

@@ -156,31 +156,11 @@ public class TestRelation extends TestRSE {
         testRSE("RelationPow1", "RelationPow1Addition.strs");
     }
 
-    @Test
-    public void testTupleProjection1() throws Exception {
-        testRSE("TupleProjection1", "TupleProjection1Addition.strs");
-    }
-
-    @Test
-    public void testTupleProjection2() throws Exception {
-        testRSE("TupleProjection2", "TupleProjection2Addition.strs");
-    }
-
-
 
+    // Sequences
     @Test
-    public void testTake() throws Exception {
-        testRSE("Take", "TakeAddition.strs");
-    }
-
-    @Test
-    public void testAppend() throws Exception {
-        testRSE("Append", "AppendAddition.strs");
-    }
-
-    @Test
-    public void testConc() throws Exception {
-        testRSE("Conc", "ConcAddition.strs");
+    public void testSizeOfSequence() throws Exception {
+        testRSE("SizeOfSequence", "SizeOfSequenceAdditions.strs");
     }
 
     @Test
@@ -189,18 +169,18 @@ public class TestRelation extends TestRSE {
     }
 
     @Test
-    public void testDrop() throws Exception {
-        testRSE("Drop", "DropAddition.strs");
+    public void testPrepend() throws Exception {
+        testRSE("Prepend", "PrependAddition.strs");
     }
 
     @Test
-    public void testEmptySequence() throws Exception {
-        testRSE("EmptySequence", "EmptySequenceAddition.strs");
+    public void testAppend() throws Exception {
+        testRSE("Append", "AppendAddition.strs");
     }
 
     @Test
-    public void testEnumeratedSequence() throws Exception {
-        testRSE("EnumeratedSequence", null);
+    public void testReverse() throws Exception {
+        testRSE("ReverseSequence", "ReverseSequenceAddition.strs");
     }
 
     @Test
@@ -208,38 +188,48 @@ public class TestRelation extends TestRSE {
         testRSE("FirstElementSequence", "FirstElementSequenceAddition.strs");
     }
 
+    @Test
+    public void testLastElementSequence() throws Exception {
+        testRSE("LastElementSequence", "LastElementSequenceAddition.strs");
+    }
+
     @Test
     public void testFrontSequence() throws Exception {
         testRSE("FrontSequence", "FrontSequenceAddition.strs");
     }
 
     @Test
-    public void testLastElementSequence() throws Exception {
-        testRSE("LastElementSequence", "LastElementSequenceAddition.strs");
+    public void testTailSequence() throws Exception {
+        testRSE("TailSequence", "TailSequenceAddition.strs");
+    }
+
+    @Test(expected = Exception.class) // would require POW(INT->INT), which embedded does not support
+    public void testConc() throws Exception {
+        testRSE("Conc", "ConcAddition.strs");
     }
 
     @Test
-    public void testPrepend() throws Exception {
-        testRSE("Prepend", "PrependAddition.strs");
+    public void testTake() throws Exception {
+        testRSE("Take", "TakeAddition.strs");
     }
 
     @Test
-    public void testReverse() throws Exception {
-        testRSE("ReverseSequence", "ReverseSequenceAddition.strs");
+    public void testDrop() throws Exception {
+        testRSE("Drop", "DropAddition.strs");
     }
 
     @Test
-    public void testSizeOfSequence() throws Exception {
-        testRSE("SizeOfSequence", null);
+    public void testEmptySequence() throws Exception {
+        testRSE("EmptySequence", "EmptySequenceAddition.strs");
     }
 
     @Test
-    public void testTailSequence() throws Exception {
-        testRSE("TailSequence", "TailSequenceAddition.strs");
+    public void testEnumeratedSequence() throws Exception {
+        testRSE("EnumeratedSequence", "EnumeratedSequenceAddition.strs");
     }
 
     @Test
     public void testSequenceOperateRelation() throws Exception {
-        testRSE("SequenceOperateRelation", "SequenceOperateRelationAddition.strs");
+        testRSE("SequenceOperateRelation", "SequenceOperateRelationAddition.strs_e");
     }
 }

src/test/resources/de/hhu/stups/codegenerator/CAN_BUS_tlc_exec.out

+T2MODE_SENSE;T2_EN;false;0
\ No newline at end of file

src/test/resources/de/hhu/stups/codegenerator/CAN_BUS_tlc_execAddition.strs

+fn main() {
+    let mut can_exec = CAN_BUS_tlc_exec::new();
+    can_exec.simulate();
+    println!("{:?};", can_exec._CAN_BUS_tlc.get_T2_mode()); //T2MODE_SENSE
+    println!("{:?};", can_exec._CAN_BUS_tlc.get_T2_state()); //T2_EN
+    println!("{};", can_exec._CAN_BUS_tlc.get_T3_enabled()); //true
+    println!("{}", can_exec._CAN_BUS_tlc.get_BUSvalue()); //0
+}

src/test/resources/de/hhu/stups/codegenerator/DropAddition.strs

 fn main() {
     let mut drop = Drop::new();
     drop.calculate();
-    println!("{}", drop.getRes());
+    let res = drop.getRes();
+    if res.card().equal(&1) && res.domain().elementOf(&1) && res.range().elementOf(&3) {
+        println!("{{(1 |-> 3)}}");
+    } else {
+        println!("wrong result!");
+    }
 }

src/test/resources/de/hhu/stups/codegenerator/EmptySequenceAddition.strs

 fn main() {
     let mut empty = EmptySequence::new();
     empty.calculate();
-    println!("{}", empty.getRes());
+    let res = empty.getRes();
+    if res.card().equal(&0) {
+        println!("{{}}");
+    } else {
+        println!("Wrong result!");
+    }
 }
\ No newline at end of file

src/test/resources/de/hhu/stups/codegenerator/EnumeratedSequence.out

+2
\ No newline at end of file

src/test/resources/de/hhu/stups/codegenerator/EnumeratedSequenceAddition.strs

+fn main() {
+    let mut seq = EnumeratedSequence::new();
+    seq.calculate();
+    println!("{}", seq.get_f().card());
+}

src/test/resources/de/hhu/stups/codegenerator/RelationPow.mch

 MACHINE RelationPow
 
+SETS EINT = {ONE, TWO, THREE}
+
 VARIABLES  f, g
 
-INVARIANT  f : POW(INT * INT) & g : POW(POW(INT * INT))
+INVARIANT  f : POW(EINT * EINT) & g : POW(POW(EINT * EINT))
 
-INITIALISATION f := {1|->2, 2|-> 3}; g := POW(f)
+INITIALISATION f := {ONE|->TWO, TWO|-> THREE}; g := POW(f)
 
 OPERATIONS
 

src/test/resources/de/hhu/stups/codegenerator/RelationPow1.mch

 MACHINE RelationPow1
 
+SETS EINT = {ONE, TWO, THREE}
+
 VARIABLES  f, g
 
-INVARIANT  f : POW(INT * INT) & g : POW(POW(INT * INT))
+INVARIANT  f : POW(EINT * EINT) & g : POW(POW(EINT * EINT))
 
-INITIALISATION f := {1|->2, 2|-> 3}; g := POW1(f)
+INITIALISATION f := {ONE|->TWO, TWO|-> THREE}; g := POW1(f)
 
 OPERATIONS
 

src/test/resources/de/hhu/stups/codegenerator/SequenceOperateRelationAddition.strs_e

+fn main() {
+    let mut sequence = SequenceOperateRelation::new();
+    sequence.calculate();
+    let res = sequence.getRes();
+    if res.card().equal(&1) && res.domain().elementOf(&1) && res.range().elementOf(&2) {
+        println!("{{(1 |-> 2)}}");
+    } else {
+        println!("wrong result!");
+    }
+}
\ No newline at end of file

src/test/resources/de/hhu/stups/codegenerator/SizeOfSequence.out

+2
\ No newline at end of file

src/test/resources/de/hhu/stups/codegenerator/SizeOfSequenceAdditions.strs

+fn main() {
+    let mut machine = SizeOfSequence::new();
+    machine.calculate();
+    println!("{}", machine.get_f().card());
+}

src/test/resources/de/hhu/stups/codegenerator/embedded/CAN_BUS_tlc_NoIntSet.mch

+MACHINE CAN_BUS_tlc_NoIntSet
+
+SETS
+  T1state={T1_EN,T1_CALC,T1_SEND,T1_WAIT};
+  T2mode={T2MODE_SENSE,T2MODE_TRANSMIT,T2MODE_RELEASE};
+  T2state={T2_EN,T2_RCV,T2_PROC,T2_CALC,T2_SEND,T2_WAIT,T2_RELEASE};
+  T3state={T3_READY,T3_WRITE,T3_RELEASE,T3_READ,T3_PROC,T3_WAIT};
+  EINT={NEG_ONE,ZERO,ONE,TWO,THREE,FOUR,FIVE}
+VARIABLES
+  BUSpriority,
+  BUSvalue,
+  BUSwrite,
+  T1_state,
+  T1_timer,
+  T1_writevalue,
+  T2_mode,
+  T2_readpriority,
+  T2_readvalue,
+  T2_state,
+  T2_timer,
+  T2_writevalue,
+  T2v,
+  T3_enabled,
+  T3_evaluated,
+  T3_readpriority,
+  T3_readvalue,
+  T3_state,
+  NATSET
+INVARIANT
+   T2v : EINT &
+   T3_evaluated : BOOL &
+   T3_enabled : BOOL &
+   T1_state : T1state &
+   T2_state : T2state &
+   T3_state : T3state &
+   T1_writevalue : EINT &
+   T2_writevalue : EINT &
+   T2_readvalue : EINT &
+   T1_timer : NATURAL &
+   T2_timer : NATURAL &
+   T2_mode : T2mode &
+   BUSvalue : EINT &
+   BUSpriority : NATSET &
+   T3_readvalue : EINT &
+   T3_readpriority : NATSET &
+   T2_readpriority : NATSET &
+   BUSwrite : NATSET +-> EINT &
+   BUSwrite /= {} &
+   ZERO : dom(BUSwrite)
+INITIALISATION
+         T2v := ZERO
+      ||
+         T3_evaluated := TRUE
+      ||
+         T3_enabled := TRUE
+      ||
+         T1_state := T1_EN
+      ||
+         T2_state := T2_EN
+      ||
+         T3_state := T3_READY
+      ||
+         T1_writevalue := ZERO
+      ||
+         T2_writevalue := ZERO
+      ||
+         T2_readvalue := ZERO
+      ||
+         T2_readpriority := ZERO
+      ||
+         T3_readvalue := ZERO
+      ||
+         T3_readpriority := ZERO
+      ||
+         T1_timer := 2
+      ||
+         T2_timer := 3
+      ||
+         BUSwrite := {ZERO |-> ZERO}
+      ||
+         BUSvalue := ZERO
+      ||
+         BUSpriority := ZERO
+      ||
+         T2_mode := T2MODE_SENSE
+      ||
+         NATSET := {ZERO,ONE,TWO,THREE,FOUR,FIVE}
+OPERATIONS
+  T1Evaluate =
+    PRE
+        /* @grd1 */ T1_timer = 0
+      & /* @grd3 */ T1_state = T1_EN
+    THEN
+         T1_timer := 0
+      ||
+         T1_state := T1_CALC
+    END;
+  T1Calculate(p) =
+    PRE
+		p : {NEG_ONE, ZERO, ONE, TWO, THREE} &
+        /* @grd2 */ T1_state = T1_CALC
+    THEN
+         T1_writevalue := p
+      ||
+         T1_state := T1_SEND
+    END;
+  T1SendResult(ppriority,pv) =
+    PRE
+        /* @grd2 */ ppriority = THREE
+      & /* @grd1 */ pv = T1_writevalue
+      & /* @grd3 */ T1_state = T1_SEND
+    THEN
+         BUSwrite := BUSwrite <+ {ppriority |-> pv}
+      ||
+         T1_state := T1_WAIT
+    END;
+  T1Wait(pt) =
+    PRE
+        /* @grd1 */ pt = 2
+      & /* @grd2 */ T1_state = T1_WAIT
+    THEN
+         T1_timer := pt
+      ||
+         T1_state := T1_EN
+    END;
+  T2Evaluate =
+    PRE
+        /* @grd1 */ T2_timer = 0
+      & /* @grd3 */ T2_state = T2_EN
+    THEN
+         T2_timer := 0
+      ||
+         T2_state := T2_RCV
+    END;
+  T2ReadBus(ppriority,pv) =
+    PRE
+        /* @grd2 */ ppriority = BUSpriority
+      & /* @grd1 */ pv = BUSvalue
+      & /* @grd3 */ T2_state = T2_RCV
+    THEN
+         T2_readvalue := pv
+      ||
+         T2_readpriority := ppriority
+      ||
+         T2_state := T2_PROC
+    END;
+  T2Reset =
+    PRE
+        /* @grd1 */ T2_readpriority = FOUR
+      & /* @grd2 */ T2_state = T2_PROC
+    THEN
+         T2_writevalue := T2v
+      ||
+         T2v := ZERO
+      ||
+         T2_state := T2_SEND
+      ||
+         T2_mode := T2MODE_TRANSMIT
+    END;
+  T2Complete =
+    PRE
+        /* @grd2 */ T2_state = T2_PROC
+      & /* @grd1 */ T2_readpriority = FIVE
+      & /* @grd3 */ T2_mode = T2MODE_TRANSMIT
+    THEN
+         T2_state := T2_RELEASE
+      ||
+         T2_mode := T2MODE_SENSE
+    END;
+  T2ReleaseBus(ppriority) =
+    PRE
+        /* @grd1 */ ppriority = T2_readpriority
+      & /* @grd3 */ ppriority : dom(BUSwrite)
+      & /* @grd4 */ T2_state = T2_RELEASE
+    THEN
+         BUSwrite := {ppriority} <<| BUSwrite
+      ||
+         T2_state := T2_WAIT
+    END;
+
+  T2Calculate =
+    PRE
+        /* @grd1 */ T2_readpriority = THREE
+      & /* @grd2 */ T2_state = T2_PROC
+    THEN
+         T2v := T2_readvalue
+      ||
+         T2_state := T2_WAIT
+    END;
+
+  T2WriteBus(ppriority,pv) =
+    PRE
+        /* @grd2 */ ppriority = FIVE
+      & /* @grd1 */ pv = T2_writevalue
+      & /* @grd3 */ T2_state = T2_SEND
+    THEN
+         BUSwrite := BUSwrite <+ {ppriority |-> pv}
+      ||
+         T2_state := T2_WAIT
+    END;
+
+  T2Wait(pt) =
+    PRE
+        /* @grd1 */ pt = 3
+      & /* @grd2 */ T2_state = T2_WAIT
+    THEN
+         T2_timer := pt
+      ||
+         T2_state := T2_EN
+    END;
+
+  T3Initiate =
+    PRE
+        /* @grd1 */ T3_state = T3_READY
+      & /* @grd2 */ T3_evaluated = FALSE
+      & /* @grd3 */ T3_enabled = TRUE
+    THEN
+         T3_state := T3_WRITE
+      ||
+         T3_enabled := FALSE
+    END;
+
+  T3Evaluate =
+    PRE
+        /* @grd1 */ T3_state = T3_READY
+      & /* @grd2 */ T3_evaluated = FALSE
+      & /* @grd3 */ T3_enabled = FALSE
+    THEN
+         T3_state := T3_READ
+    END;
+
+  T3writebus(ppriority,pv) =
+    PRE
+         /* @grd2 */ ppriority = FOUR
+      &  /* @grd1 */ pv = ZERO
+      & /* @grd3 */ T3_state = T3_WRITE
+    THEN
+         BUSwrite := BUSwrite <+ {ppriority |-> pv}
+      ||
+         T3_state := T3_WAIT
+    END;
+
+  T3Read(ppriority,pv) =
+    PRE
+        /* @grd2 */ ppriority = BUSpriority
+      & /* @grd1 */ pv = BUSvalue
+      & /* @grd4 */ T3_state = T3_READ
+    THEN
+         T3_readvalue := pv
+      ||
+         T3_readpriority := ppriority
+      ||
+         T3_state := T3_PROC
+    END;
+
+  T3Poll =
+    PRE
+        /* @grd1 */ T3_readpriority : EINT \ {FIVE}
+      & /* @grd2 */ T3_state = T3_PROC
+    THEN
+         T3_state := T3_WAIT
+    END;
+
+  T3ReleaseBus(ppriority) =
+    PRE
+        /* @grd1 */ ppriority = FOUR
+      & /* @grd2 */ T3_readpriority = FIVE
+      & /* @grd3 */ T3_state = T3_PROC
+    THEN
+         BUSwrite := {ppriority} <<| BUSwrite
+      ||
+         T3_state := T3_RELEASE
+    END;
+
+  T3Wait =
+    PRE
+        /* @grd1 */ T3_state = T3_WAIT
+    THEN
+         T3_state := T3_READY
+      ||
+         T3_evaluated := TRUE
+    END;
+
+  T3ReEnableWait =
+    PRE
+        /* @grd1 */ T3_state = T3_RELEASE
+    THEN
+         T3_state := T3_READY
+      ||
+         T3_evaluated := TRUE
+      ||
+         T3_enabled := TRUE
+    END;
+
+  Update(pmax) =
+    PRE
+        /* @grd1 */ pmax = IF FIVE : dom(BUSwrite) THEN FIVE
+                           ELSE IF FOUR : dom(BUSwrite) THEN FOUR
+                           ELSE IF THREE : dom(BUSwrite) THEN THREE
+                           ELSE IF TWO : dom(BUSwrite) THEN TWO
+                           ELSE IF ONE : dom(BUSwrite) THEN ONE ELSE ZERO END END END END END/* max(dom(BUSwrite)) */
+      & /* @grd2 */ T1_timer > 0
+      & /* @grd3 */ T2_timer > 0
+      & (/* @grd4 */ T3_enabled = TRUE or T3_evaluated = TRUE)
+    THEN
+         BUSvalue := BUSwrite(pmax)
+      ||
+         BUSpriority := pmax
+      ||
+         T1_timer := T1_timer - 1
+      ||
+         T2_timer := T2_timer - 1
+      ||
+         T3_evaluated := FALSE
+    END
+
+END
\ No newline at end of file