Add benchmarks for python generated machines

benchmarks/Python_Primitives/CAN_BUS_tlc.py

+from btypes.BBoolean import BBoolean
+from btypes.BSet import BSet
+from btypes.BInteger import BInteger
+from btypes.BRelation import BRelation
+from btypes.BTuple import BTuple
+from btypes.BObject import BObject
+
+
+from enum import Enum, auto
+
+
+class T1state(BObject, Enum):
+    T1_EN = auto()
+    T1_CALC = auto()
+    T1_SEND = auto()
+    T1_WAIT = auto()
+
+
+    def equal(self, o):
+        return BBoolean(self == o)
+
+    def unequal(self, o):
+        return BBoolean(self != o)
+
+    def __str__(self):
+                if self == T1state.T1_EN:
+                    return "T1_EN"
+                if self == T1state.T1_CALC:
+                    return "T1_CALC"
+                if self == T1state.T1_SEND:
+                    return "T1_SEND"
+                if self == T1state.T1_WAIT:
+                    return "T1_WAIT"
+
+
+from enum import Enum, auto
+
+
+class T2mode(BObject, Enum):
+    T2MODE_SENSE = auto()
+    T2MODE_TRANSMIT = auto()
+    T2MODE_RELEASE = auto()
+
+
+    def equal(self, o):
+        return BBoolean(self == o)
+
+    def unequal(self, o):
+        return BBoolean(self != o)
+
+    def __str__(self):
+                if self == T2mode.T2MODE_SENSE:
+                    return "T2MODE_SENSE"
+                if self == T2mode.T2MODE_TRANSMIT:
+                    return "T2MODE_TRANSMIT"
+                if self == T2mode.T2MODE_RELEASE:
+                    return "T2MODE_RELEASE"
+
+
+from enum import Enum, auto
+
+
+class T2state(BObject, Enum):
+    T2_EN = auto()
+    T2_RCV = auto()
+    T2_PROC = auto()
+    T2_CALC = auto()
+    T2_SEND = auto()
+    T2_WAIT = auto()
+    T2_RELEASE = auto()
+
+    def equal(self, o):
+        return BBoolean(self == o)
+
+    def unequal(self, o):
+        return BBoolean(self != o)
+
+    def __str__(self):
+                if self == T2state.T2_EN:
+                    return "T2_EN"
+                if self == T2state.T2_RCV:
+                    return "T2_RCV"
+                if self == T2state.T2_PROC:
+                    return "T2_PROC"
+                if self == T2state.T2_CALC:
+                    return "T2_CALC"
+                if self == T2state.T2_SEND:
+                    return "T2_SEND"
+                if self == T2state.T2_WAIT:
+                    return "T2_WAIT"
+                if self == T2state.T2_RELEASE:
+                    return "T2_RELEASE"
+
+
+from enum import Enum, auto
+
+
+class T3state(BObject, Enum):
+    T3_READY = auto()
+    T3_WRITE = auto()
+    T3_RELEASE = auto()
+    T3_READ = auto()
+    T3_PROC = auto()
+    T3_WAIT = auto()
+
+    def equal(self, o):
+        return BBoolean(self == o)
+
+    def unequal(self, o):
+        return BBoolean(self != o)
+
+    def __str__(self):
+                if self == T3state.T3_READY:
+                    return "T3_READY"
+                if self == T3state.T3_WRITE:
+                    return "T3_WRITE"
+                if self == T3state.T3_RELEASE:
+                    return "T3_RELEASE"
+                if self == T3state.T3_READ:
+                    return "T3_READ"
+                if self == T3state.T3_PROC:
+                    return "T3_PROC"
+                if self == T3state.T3_WAIT:
+                    return "T3_WAIT"
+
+
+class CAN_BUS_tlc:
+
+
+
+    _T1state = BSet(T1state.T1_EN, T1state.T1_CALC, T1state.T1_SEND, T1state.T1_WAIT)
+    _T2mode = BSet(T2mode.T2MODE_SENSE, T2mode.T2MODE_TRANSMIT, T2mode.T2MODE_RELEASE)
+    _T2state = BSet(T2state.T2_EN, T2state.T2_RCV, T2state.T2_PROC, T2state.T2_CALC, T2state.T2_SEND, T2state.T2_WAIT, T2state.T2_RELEASE)
+    _T3state = BSet(T3state.T3_READY, T3state.T3_WRITE, T3state.T3_RELEASE, T3state.T3_READ, T3state.T3_PROC, T3state.T3_WAIT)
+
+    def __init__(self):
+        NATSET = BSet.interval(BInteger(0),BInteger(5))
+        self.T2v = BInteger(0)
+        self.T3_evaluated = BBoolean(True)
+        self.T3_enabled = BBoolean(True)
+        self.T1_state = T1state.T1_EN
+        self.T2_state = T2state.T2_EN
+        self.T3_state = T3state.T3_READY
+        self.T1_writevalue = BInteger(0)
+        self.T2_writevalue = BInteger(0)
+        self.T2_readvalue = BInteger(0)
+        self.T2_readpriority = BInteger(0)
+        self.T3_readvalue = BInteger(0)
+        self.T3_readpriority = BInteger(0)
+        self.T1_timer = BInteger(2)
+        self.T2_timer = BInteger(3)
+        self.BUSwrite = BRelation(BTuple(BInteger(0), BInteger(0)))
+        self.BUSvalue = BInteger(0)
+        self.BUSpriority = BInteger(0)
+        self.T2_mode = T2mode.T2MODE_SENSE
+
+    def T1Evaluate(self):
+        self.T1_timer = BInteger(0)
+        self.T1_state = T1state.T1_CALC
+
+    def T1Calculate(self, p):
+        self.T1_writevalue = p
+        self.T1_state = T1state.T1_SEND
+
+    def T1SendResult(self, ppriority, pv):
+        _ld_BUSwrite = self.BUSwrite
+        self.BUSwrite = _ld_BUSwrite.override(BRelation(BTuple(ppriority, pv)))
+        self.T1_state = T1state.T1_WAIT
+
+    def T1Wait(self, pt):
+        self.T1_timer = pt
+        self.T1_state = T1state.T1_EN
+
+    def T2Evaluate(self):
+        self.T2_timer = BInteger(0)
+        self.T2_state = T2state.T2_RCV
+
+    def T2ReadBus(self, ppriority, pv):
+        self.T2_readvalue = pv
+        self.T2_readpriority = ppriority
+        self.T2_state = T2state.T2_PROC
+
+    def T2Reset(self):
+        _ld_T2v = self.T2v
+        self.T2_writevalue = _ld_T2v
+        self.T2v = BInteger(0)
+        self.T2_state = T2state.T2_SEND
+        self.T2_mode = T2mode.T2MODE_TRANSMIT
+
+    def T2Complete(self):
+        self.T2_state = T2state.T2_RELEASE
+        self.T2_mode = T2mode.T2MODE_SENSE
+
+    def T2ReleaseBus(self, ppriority):
+        _ld_BUSwrite = self.BUSwrite
+        self.BUSwrite = _ld_BUSwrite.domainSubstraction(BSet(ppriority))
+        self.T2_state = T2state.T2_WAIT
+
+    def T2Calculate(self):
+        self.T2v = self.T2_readvalue
+        self.T2_state = T2state.T2_WAIT
+
+    def T2WriteBus(self, ppriority, pv):
+        _ld_BUSwrite = self.BUSwrite
+        self.BUSwrite = _ld_BUSwrite.override(BRelation(BTuple(ppriority, pv)))
+        self.T2_state = T2state.T2_WAIT
+
+    def T2Wait(self, pt):
+        self.T2_timer = pt
+        self.T2_state = T2state.T2_EN
+
+    def T3Initiate(self):
+        self.T3_state = T3state.T3_WRITE
+        self.T3_enabled = BBoolean(False)
+
+    def T3Evaluate(self):
+        self.T3_state = T3state.T3_READ
+
+    def T3writebus(self, ppriority, pv):
+        _ld_BUSwrite = self.BUSwrite
+        self.BUSwrite = _ld_BUSwrite.override(BRelation(BTuple(ppriority, pv)))
+        self.T3_state = T3state.T3_WAIT
+
+    def T3Read(self, ppriority, pv):
+        self.T3_readvalue = pv
+        self.T3_readpriority = ppriority
+        self.T3_state = T3state.T3_PROC
+
+    def T3Poll(self):
+        self.T3_state = T3state.T3_WAIT
+
+    def T3ReleaseBus(self, ppriority):
+        _ld_BUSwrite = self.BUSwrite
+        self.BUSwrite = _ld_BUSwrite.domainSubstraction(BSet(ppriority))
+        self.T3_state = T3state.T3_RELEASE
+
+    def T3Wait(self):
+        self.T3_state = T3state.T3_READY
+        self.T3_evaluated = BBoolean(True)
+
+    def T3ReEnableWait(self):
+        self.T3_state = T3state.T3_READY
+        self.T3_evaluated = BBoolean(True)
+        self.T3_enabled = BBoolean(True)
+
+    def Update(self, pmax):
+        _ld_T2_timer = self.T2_timer
+        _ld_T1_timer = self.T1_timer
+        self.BUSvalue = self.BUSwrite.functionCall(pmax)
+        self.BUSpriority = pmax
+        self.T1_timer = _ld_T1_timer.minus(BInteger(1))
+        self.T2_timer = _ld_T2_timer.minus(BInteger(1))
+        self.T3_evaluated = BBoolean(False)
+
+    def _get_BUSpriority(self):
+        return self.BUSpriority
+
+    def _get_BUSvalue(self):
+        return self.BUSvalue
+
+    def _get_BUSwrite(self):
+        return self.BUSwrite
+
+    def _get_T1_state(self):
+        return self.T1_state
+
+    def _get_T1_timer(self):
+        return self.T1_timer
+
+    def _get_T1_writevalue(self):
+        return self.T1_writevalue
+
+    def _get_T2_mode(self):
+        return self.T2_mode
+
+    def _get_T2_readpriority(self):
+        return self.T2_readpriority
+
+    def _get_T2_readvalue(self):
+        return self.T2_readvalue
+
+    def _get_T2_state(self):
+        return self.T2_state
+
+    def _get_T2_timer(self):
+        return self.T2_timer
+
+    def _get_T2_writevalue(self):
+        return self.T2_writevalue
+
+    def _get_T2v(self):
+        return self.T2v
+
+    def _get_T3_enabled(self):
+        return self.T3_enabled
+
+    def _get_T3_evaluated(self):
+        return self.T3_evaluated
+
+    def _get_T3_readpriority(self):
+        return self.T3_readpriority
+
+    def _get_T3_readvalue(self):
+        return self.T3_readvalue
+
+    def _get_T3_state(self):
+        return self.T3_state
+
+

benchmarks/Python_Primitives/Lift.py

+from btypes.BInteger import BInteger
+
+
+
+class Lift:
+
+
+
+
+    def __init__(self):
+        self.floor = BInteger(0)
+
+    def inc(self):
+        self.floor = self.floor.plus(BInteger(1))
+
+
+    def dec(self):
+        self.floor = self.floor.minus(BInteger(1))
+
+
+    def _get_floor(self):
+        return self.floor
+
+

benchmarks/Python_Primitives/LiftExec.py

+from btypes.BBoolean import BBoolean
+from btypes.BInteger import BInteger
+from Lift import Lift
+
+
+
+class LiftExec:
+
+
+
+
+    def __init__(self):
+        self._Lift = Lift()
+
+        self.counter = BInteger(0)
+
+    def simulate(self):
+        while((self.counter.less(BInteger(3000))).booleanValue()):
+            i = None
+            i = BInteger(0)
+            while((i.less(BInteger(100))).booleanValue()):
+                self._Lift.inc()
+                i = i.plus(BInteger(1))
+
+            _i = None
+            _i = BInteger(0)
+            while((_i.less(BInteger(100))).booleanValue()):
+                self._Lift.dec()
+                _i = _i.plus(BInteger(1))
+
+            self.counter = self.counter.plus(BInteger(1))
+
+
+
+    def getCounter(self):
+        out = None
+        out = self.counter
+        return out
+
+
+
+if __name__ == "__main__":
+    lift = LiftExec();
+    lift.simulate()
+    print(lift.getCounter())
\ No newline at end of file

benchmarks/Python_Primitives/Makefile

+.SUFFIXES:
+
+.PHONY: all
+
+all: CAN_BUS_tlc_exec Cruise_finite1_deterministic_exec LiftExec scheduler_deterministic_exec Sieve TrafficLightExec Train_1_beebook_deterministic_exec sort_m2_data1000_exec
+
+BTYPESPYTHON=../../btypes_primitives/src/main/python_immutable2
+OUTPUT ?= runtimes.txt
+
+% : export PYTHONPATH = $(BTYPESPYTHON)
+% :
+	/usr/bin/time -f "%C %E %M" -ao $(OUTPUT) python $@.py

benchmarks/Python_Primitives/Sieve.py

+from btypes.BBoolean import BBoolean
+from btypes.BSet import BSet
+from btypes.BInteger import BInteger
+
+class Sieve:
+
+    def __init__(self):
+        li = 2000000
+        self.numbers = BSet.interval(BInteger(2), BInteger(li))
+        self.cur = BInteger(2)
+        self.limit = BInteger(li)
+
+    def ComputeNumberOfPrimes(self):
+        while (BBoolean(self.cur.greater(BInteger(1)).booleanValue() and self.cur.multiply(self.cur).lessEqual(self.limit).booleanValue())).booleanValue():
+            if (self.numbers.elementOf(self.cur)).booleanValue():
+                n = self.cur
+                set = BSet()
+                while (n.lessEqual(self.limit.divide(self.cur))).booleanValue():
+                    set = set.union(BSet(self.cur.multiply(n)))
+                    n = n.plus(BInteger(1))
+
+                self.numbers = self.numbers.difference(set)
+
+            self.cur = self.cur.plus(BInteger(1))
+
+        res = self.numbers.card()
+        return res
+
+
+if __name__ == '__main__':
+    sieve = Sieve()
+    print(sieve.ComputeNumberOfPrimes())

benchmarks/Python_Primitives/TrafficLightExec.py

@@ -3,19 +3,15 @@ from btypes.BInteger import BInteger
 from TrafficLight import TrafficLight
 
 
-
 class TrafficLightExec:
 
-
-
-
     def __init__(self):
         self._TrafficLight = TrafficLight()
 
         self.counter = BInteger(0)
 
     def simulate(self):
-        while((self.counter.less(BInteger(300000000))).booleanValue()):
+        while (self.counter.less(BInteger(300000000))).booleanValue():
             self._TrafficLight.cars_ry()
             self._TrafficLight.cars_g()
             self._TrafficLight.cars_y()

benchmarks/Python_Primitives/Train_1_beebook_deterministic.py

+from btypes.BBoolean import BBoolean
+from btypes.BSet import BSet
+from btypes.BInteger import BInteger
+from btypes.BRelation import BRelation
+from btypes.BTuple import BTuple
+from btypes.BObject import BObject
+
+
+from enum import Enum, auto
+class BLOCKS(BObject, Enum):
+    A = auto()
+    B = auto()
+    C = auto()
+    D = auto()
+    E = auto()
+    F = auto()
+    G = auto()
+    H = auto()
+    I = auto()
+    J = auto()
+    K = auto()
+    L = auto()
+    M = auto()
+    N = auto()
+
+
+    def equal(self, o):
+        return BBoolean(self == o)
+
+    def unequal(self, o):
+        return BBoolean(self != o)
+
+    def __str__(self):
+                if self == BLOCKS.A:
+                    return "A"
+                if self == BLOCKS.B:
+                    return "B"
+                if self == BLOCKS.C:
+                    return "C"
+                if self == BLOCKS.D:
+                    return "D"
+                if self == BLOCKS.E:
+                    return "E"
+                if self == BLOCKS.F:
+                    return "F"
+                if self == BLOCKS.G:
+                    return "G"
+                if self == BLOCKS.H:
+                    return "H"
+                if self == BLOCKS.I:
+                    return "I"
+                if self == BLOCKS.J:
+                    return "J"
+                if self == BLOCKS.K:
+                    return "K"
+                if self == BLOCKS.L:
+                    return "L"
+                if self == BLOCKS.M:
+                    return "M"
+                if self == BLOCKS.N:
+                    return "N"
+
+
+from enum import Enum, auto
+class ROUTES(BObject, Enum):
+    R1 = auto()
+    R2 = auto()
+    R3 = auto()
+    R4 = auto()
+    R5 = auto()
+    R6 = auto()
+    R7 = auto()
+    R8 = auto()
+    R9 = auto()
+    R10 = auto()
+
+
+    def equal(self, o):
+        return BBoolean(self == o)
+
+    def unequal(self, o):
+        return BBoolean(self != o)
+
+    def __str__(self):
+                if self == ROUTES.R1:
+                    return "R1"
+                if self == ROUTES.R2:
+                    return "R2"
+                if self == ROUTES.R3:
+                    return "R3"
+                if self == ROUTES.R4:
+                    return "R4"
+                if self == ROUTES.R5:
+                    return "R5"
+                if self == ROUTES.R6:
+                    return "R6"
+                if self == ROUTES.R7:
+                    return "R7"
+                if self == ROUTES.R8:
+                    return "R8"
+                if self == ROUTES.R9:
+                    return "R9"
+                if self == ROUTES.R10:
+                    return "R10"
+
+
+class Train_1_beebook_deterministic:
+
+
+
+    _BLOCKS = BSet(BLOCKS.A, BLOCKS.B, BLOCKS.C, BLOCKS.D, BLOCKS.E, BLOCKS.F, BLOCKS.G, BLOCKS.H, BLOCKS.I, BLOCKS.J, BLOCKS.K, BLOCKS.L, BLOCKS.M, BLOCKS.N)
+    _ROUTES = BSet(ROUTES.R1, ROUTES.R2, ROUTES.R3, ROUTES.R4, ROUTES.R5, ROUTES.R6, ROUTES.R7, ROUTES.R8, ROUTES.R9, ROUTES.R10)
+
+    def __init__(self):
+        fst = BRelation(BTuple(ROUTES.R1, BLOCKS.L), BTuple(ROUTES.R2, BLOCKS.L), BTuple(ROUTES.R3, BLOCKS.L), BTuple(ROUTES.R4, BLOCKS.M), BTuple(ROUTES.R5, BLOCKS.M), BTuple(ROUTES.R6, BLOCKS.C), BTuple(ROUTES.R7, BLOCKS.G), BTuple(ROUTES.R8, BLOCKS.N), BTuple(ROUTES.R9, BLOCKS.G), BTuple(ROUTES.R10, BLOCKS.N))
+        lst = BRelation(BTuple(ROUTES.R1, BLOCKS.C), BTuple(ROUTES.R2, BLOCKS.G), BTuple(ROUTES.R3, BLOCKS.N), BTuple(ROUTES.R4, BLOCKS.G), BTuple(ROUTES.R5, BLOCKS.N), BTuple(ROUTES.R6, BLOCKS.L), BTuple(ROUTES.R7, BLOCKS.L), BTuple(ROUTES.R8, BLOCKS.L), BTuple(ROUTES.R9, BLOCKS.M), BTuple(ROUTES.R10, BLOCKS.M))
+        nxt = BRelation(BTuple(ROUTES.R1, BRelation(BTuple(BLOCKS.L, BLOCKS.A), BTuple(BLOCKS.A, BLOCKS.B), BTuple(BLOCKS.B, BLOCKS.C))), BTuple(ROUTES.R2, BRelation(BTuple(BLOCKS.L, BLOCKS.A), BTuple(BLOCKS.A, BLOCKS.B), BTuple(BLOCKS.B, BLOCKS.D), BTuple(BLOCKS.D, BLOCKS.E), BTuple(BLOCKS.E, BLOCKS.F), BTuple(BLOCKS.F, BLOCKS.G))), BTuple(ROUTES.R3, BRelation(BTuple(BLOCKS.L, BLOCKS.A), BTuple(BLOCKS.A, BLOCKS.B), BTuple(BLOCKS.B, BLOCKS.D), BTuple(BLOCKS.D, BLOCKS.K), BTuple(BLOCKS.K, BLOCKS.J), BTuple(BLOCKS.J, BLOCKS.N))), BTuple(ROUTES.R4, BRelation(BTuple(BLOCKS.M, BLOCKS.H), BTuple(BLOCKS.H, BLOCKS.I), BTuple(BLOCKS.I, BLOCKS.K), BTuple(BLOCKS.K, BLOCKS.F), BTuple(BLOCKS.F, BLOCKS.G))), BTuple(ROUTES.R5, BRelation(BTuple(BLOCKS.M, BLOCKS.H), BTuple(BLOCKS.H, BLOCKS.I), BTuple(BLOCKS.I, BLOCKS.J), BTuple(BLOCKS.J, BLOCKS.N))), BTuple(ROUTES.R6, BRelation(BTuple(BLOCKS.C, BLOCKS.B), BTuple(BLOCKS.B, BLOCKS.A), BTuple(BLOCKS.A, BLOCKS.L))), BTuple(ROUTES.R7, BRelation(BTuple(BLOCKS.G, BLOCKS.F), BTuple(BLOCKS.F, BLOCKS.E), BTuple(BLOCKS.E, BLOCKS.D), BTuple(BLOCKS.D, BLOCKS.B), BTuple(BLOCKS.B, BLOCKS.A), BTuple(BLOCKS.A, BLOCKS.L))), BTuple(ROUTES.R8, BRelation(BTuple(BLOCKS.N, BLOCKS.J), BTuple(BLOCKS.J, BLOCKS.K), BTuple(BLOCKS.K, BLOCKS.D), BTuple(BLOCKS.D, BLOCKS.B), BTuple(BLOCKS.B, BLOCKS.A), BTuple(BLOCKS.A, BLOCKS.L))), BTuple(ROUTES.R9, BRelation(BTuple(BLOCKS.G, BLOCKS.F), BTuple(BLOCKS.F, BLOCKS.K), BTuple(BLOCKS.K, BLOCKS.I), BTuple(BLOCKS.I, BLOCKS.H), BTuple(BLOCKS.H, BLOCKS.M))), BTuple(ROUTES.R10, BRelation(BTuple(BLOCKS.N, BLOCKS.J), BTuple(BLOCKS.J, BLOCKS.I), BTuple(BLOCKS.I, BLOCKS.H), BTuple(BLOCKS.H, BLOCKS.M))))
+        self._ic_set_0 = BRelation()
+        for _ic_b_1 in self._BLOCKS:
+            for _ic_r_1 in self._ROUTES:
+                if(BBoolean(nxt.domain().elementOf(_ic_r_1).booleanValue() and BBoolean(nxt.functionCall(_ic_r_1).domain().elementOf(_ic_b_1).booleanValue() or nxt.functionCall(_ic_r_1)._range().elementOf(_ic_b_1).booleanValue()).booleanValue())).booleanValue():
+                    _ic_set_0 = _ic_set_0.union(BRelation(BTuple(_ic_b_1, _ic_r_1)))
+
+        rtbl = _ic_set_0
+        self.resrt = BSet()
+        self.resbl = BSet()
+        self.rsrtbl = BRelation()
+        self.OCC = BSet()
+        self.TRK = BRelation()
+        self.frm = BSet()
+        self.LBT = BSet()
+        self.visited = BSet()
+
+    def route_reservation(self, r):
+        _ld_resrt = self.resrt
+
+        _ld_rsrtbl = self.rsrtbl
+        _ld_visited = self.visited
+        _ld_resbl = self.resbl
+        self.resrt = _ld_resrt.union(BSet(r))
+        self.rsrtbl = _ld_rsrtbl.union(rtbl.rangeRestriction(BSet(r)))
+        self.resbl = _ld_resbl.union(rtbl.inverse().relationImage(BSet(r)))
+        self.visited = _ld_visited.union(BSet(BInteger(1)))
+
+
+    def route_freeing(self, r):
+        _ld_resrt = self.resrt
+
+        _ld_frm = self.frm
+        _ld_visited = self.visited
+        self.resrt = _ld_resrt.difference(BSet(r))
+        self.frm = _ld_frm.difference(BSet(r))
+        self.visited = _ld_visited.union(BSet(BInteger(2)))
+
+
+    def FRONT_MOVE_1(self, r):
+        _ld_OCC = self.OCC
+        _ld_LBT = self.LBT
+        _ld_visited = self.visited
+        self.OCC = _ld_OCC.union(BSet(fst.functionCall(r)))
+        self.LBT = _ld_LBT.union(BSet(fst.functionCall(r)))
+        self.visited = _ld_visited.union(BSet(BInteger(3)))
+
+
+    def FRONT_MOVE_2(self, b):
+        _ld_OCC = self.OCC
+        _ld_visited = self.visited
+        self.OCC = _ld_OCC.union(BSet(self.TRK.functionCall(b)))
+        self.visited = _ld_visited.union(BSet(BInteger(4)))
+
+
+    def BACK_MOVE_1(self, b):
+        _ld_OCC = self.OCC
+        _ld_LBT = self.LBT
+        _ld_rsrtbl = self.rsrtbl
+        _ld_visited = self.visited
+        _ld_resbl = self.resbl
+        self.OCC = _ld_OCC.difference(BSet(b))
+        self.rsrtbl = _ld_rsrtbl.domainSubstraction(BSet(b))
+        self.resbl = _ld_resbl.difference(BSet(b))
+        self.LBT = _ld_LBT.difference(BSet(b))
+        self.visited = _ld_visited.union(BSet(BInteger(5)))
+
+
+    def BACK_MOVE_2(self, b):
+        _ld_OCC = self.OCC
+        _ld_LBT = self.LBT
+        _ld_rsrtbl = self.rsrtbl
+        _ld_visited = self.visited
+        _ld_resbl = self.resbl
+        self.OCC = _ld_OCC.difference(BSet(b))
+        self.rsrtbl = _ld_rsrtbl.domainSubstraction(BSet(b))
+        self.resbl = _ld_resbl.difference(BSet(b))
+        self.LBT = _ld_LBT.difference(BSet(b)).union(BSet(self.TRK.functionCall(b)))
+        self.visited = _ld_visited.union(BSet(BInteger(6)))
+
+
+    def point_positionning(self, r):
+        _ld_TRK = self.TRK
+        _ld_visited = self.visited
+        self.TRK = _ld_TRK.domainSubstraction(nxt.functionCall(r).domain()).rangeSubstraction(nxt.functionCall(r)._range()).union(nxt.functionCall(r))
+        self.visited = _ld_visited.union(BSet(BInteger(7)))
+
+
+    def route_formation(self, r):
+        _ld_frm = self.frm
+        _ld_visited = self.visited
+        self.frm = _ld_frm.union(BSet(r))
+        self.visited = _ld_visited.union(BSet(BInteger(8)))
+
+
+    def _get_LBT(self):
+        return self.LBT
+
+    def _get_TRK(self):
+        return self.TRK
+
+    def _get_frm(self):
+        return self.frm
+
+    def _get_OCC(self):
+        return self.OCC
+
+    def _get_resbl(self):
+        return self.resbl
+
+    def _get_resrt(self):
+        return self.resrt
+
+    def _get_rsrtbl(self):
+        return self.rsrtbl
+
+    def _get_visited(self):
+        return self.visited
+
+

benchmarks/Python_Primitives/Train_1_beebook_deterministic_exec.py

+from btypes.BBoolean import BBoolean
+from btypes.BInteger import BInteger
+from btypes.BObject import BObject
+from Train_1_beebook_deterministic import Train_1_beebook_deterministic
+
+
+
+class Train_1_beebook_deterministic_exec:
+
+
+
+
+    def __init__(self):
+        self._Train_1_beebook_deterministic = Train_1_beebook_deterministic()
+
+        self.counter = BInteger(0)
+
+    def simulate(self):
+        while((self.counter.less(BInteger(1000))).booleanValue()):
+            self._Train_1_beebook_deterministic.route_reservation(Train_1_beebook_deterministic.ROUTES.R1)
+            self._Train_1_beebook_deterministic.route_reservation(Train_1_beebook_deterministic.ROUTES.R4)
+            self._Train_1_beebook_deterministic.point_positionning(Train_1_beebook_deterministic.ROUTES.R1)
+            self._Train_1_beebook_deterministic.point_positionning(Train_1_beebook_deterministic.ROUTES.R4)
+            self._Train_1_beebook_deterministic.route_formation(Train_1_beebook_deterministic.ROUTES.R1)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_1(Train_1_beebook_deterministic.ROUTES.R1)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.L)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.A)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.B)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.L)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.A)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.B)
+            self._Train_1_beebook_deterministic.BACK_MOVE_1(Train_1_beebook_deterministic.BLOCKS.C)
+            self._Train_1_beebook_deterministic.route_reservation(Train_1_beebook_deterministic.ROUTES.R6)
+            self._Train_1_beebook_deterministic.route_freeing(Train_1_beebook_deterministic.ROUTES.R1)
+            self._Train_1_beebook_deterministic.route_formation(Train_1_beebook_deterministic.ROUTES.R4)
+            self._Train_1_beebook_deterministic.point_positionning(Train_1_beebook_deterministic.ROUTES.R6)
+            self._Train_1_beebook_deterministic.route_formation(Train_1_beebook_deterministic.ROUTES.R6)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_1(Train_1_beebook_deterministic.ROUTES.R4)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.M)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_1(Train_1_beebook_deterministic.ROUTES.R6)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.C)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.H)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.C)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.M)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.I)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.H)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.B)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.B)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.I)
+            self._Train_1_beebook_deterministic.route_reservation(Train_1_beebook_deterministic.ROUTES.R5)
+            self._Train_1_beebook_deterministic.point_positionning(Train_1_beebook_deterministic.ROUTES.R5)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.A)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.K)
+            self._Train_1_beebook_deterministic.route_formation(Train_1_beebook_deterministic.ROUTES.R5)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.A)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.K)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.F)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.F)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_1(Train_1_beebook_deterministic.ROUTES.R5)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.M)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.M)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.H)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.H)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.I)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.J)
+            self._Train_1_beebook_deterministic.BACK_MOVE_1(Train_1_beebook_deterministic.BLOCKS.L)
+            self._Train_1_beebook_deterministic.BACK_MOVE_1(Train_1_beebook_deterministic.BLOCKS.G)
+            self._Train_1_beebook_deterministic.route_reservation(Train_1_beebook_deterministic.ROUTES.R1)
+            self._Train_1_beebook_deterministic.point_positionning(Train_1_beebook_deterministic.ROUTES.R1)
+            self._Train_1_beebook_deterministic.route_formation(Train_1_beebook_deterministic.ROUTES.R1)
+            self._Train_1_beebook_deterministic.route_freeing(Train_1_beebook_deterministic.ROUTES.R4)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.I)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.J)
+            self._Train_1_beebook_deterministic.route_freeing(Train_1_beebook_deterministic.ROUTES.R6)
+            self._Train_1_beebook_deterministic.route_reservation(Train_1_beebook_deterministic.ROUTES.R9)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_1(Train_1_beebook_deterministic.ROUTES.R1)
+            self._Train_1_beebook_deterministic.BACK_MOVE_1(Train_1_beebook_deterministic.BLOCKS.N)
+            self._Train_1_beebook_deterministic.point_positionning(Train_1_beebook_deterministic.ROUTES.R9)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.L)
+            self._Train_1_beebook_deterministic.route_formation(Train_1_beebook_deterministic.ROUTES.R9)
+            self._Train_1_beebook_deterministic.route_freeing(Train_1_beebook_deterministic.ROUTES.R5)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.L)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.A)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_1(Train_1_beebook_deterministic.ROUTES.R9)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.B)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.G)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.A)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.G)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.B)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.F)
+            self._Train_1_beebook_deterministic.BACK_MOVE_1(Train_1_beebook_deterministic.BLOCKS.C)
+            self._Train_1_beebook_deterministic.route_reservation(Train_1_beebook_deterministic.ROUTES.R6)
+            self._Train_1_beebook_deterministic.point_positionning(Train_1_beebook_deterministic.ROUTES.R6)
+            self._Train_1_beebook_deterministic.route_formation(Train_1_beebook_deterministic.ROUTES.R6)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.F)
+            self._Train_1_beebook_deterministic.route_freeing(Train_1_beebook_deterministic.ROUTES.R1)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.K)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.I)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.H)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_1(Train_1_beebook_deterministic.ROUTES.R6)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.C)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.B)
+            self._Train_1_beebook_deterministic.FRONT_MOVE_2(Train_1_beebook_deterministic.BLOCKS.A)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.K)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.I)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.H)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.C)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.B)
+            self._Train_1_beebook_deterministic.BACK_MOVE_2(Train_1_beebook_deterministic.BLOCKS.A)
+            self._Train_1_beebook_deterministic.BACK_MOVE_1(Train_1_beebook_deterministic.BLOCKS.L)
+            self._Train_1_beebook_deterministic.BACK_MOVE_1(Train_1_beebook_deterministic.BLOCKS.M)
+            self._Train_1_beebook_deterministic.route_freeing(Train_1_beebook_deterministic.ROUTES.R6)
+            self._Train_1_beebook_deterministic.route_freeing(Train_1_beebook_deterministic.ROUTES.R9)
+            self.counter = self.counter.plus(BInteger(1))
+
+
+
+
+

benchmarks/Python_Primitives/scheduler_deterministic.py

+from btypes.BBoolean import BBoolean
+from btypes.BSet import BSet
+from btypes.BObject import BObject
+
+
+from enum import Enum, auto
+class PID(BObject, Enum):
+    process1 = auto()
+    process2 = auto()
+    process3 = auto()
+
+
+    def equal(self, o):
+        return BBoolean(self == o)
+
+    def unequal(o):
+        return BBoolean(self != o)
+
+    def __str__(self):
+                if self == PID.process1:
+                    return "process1"
+                if self == PID.process2:
+                    return "process2"
+                if self == PID.process3:
+                    return "process3"
+
+
+class scheduler_deterministic:
+
+
+
+    _PID = BSet(PID.process1, PID.process2, PID.process3)
+
+    def __init__(self):
+        self.active = BSet()
+        self._ready = BSet()
+        self.waiting = BSet()
+
+    def new(self, pp):
+        if((BBoolean(BBoolean(self._PID.elementOf(pp).booleanValue() and self.active.notElementOf(pp).booleanValue()).booleanValue() and self._ready.union(self.waiting).notElementOf(pp).booleanValue())).booleanValue()):
+            self.waiting = self.waiting.union(BSet(pp))
+
+
+    def _del(self, pp):
+        if((self.waiting.elementOf(pp)).booleanValue()):
+            self.waiting = self.waiting.difference(BSet(pp))
+
+
+    def ready(self, rr):
+        if((self.waiting.elementOf(rr)).booleanValue()):
+            self.waiting = self.waiting.difference(BSet(rr))
+            if((self.active.equal(BSet())).booleanValue()):
+                self.active = BSet(rr)
+            else:
+                self._ready = self._ready.union(BSet(rr))
+
+
+    def swap(self, pp):
+        if((self.active.unequal(BSet())).booleanValue()):
+            self.waiting = self.waiting.union(self.active)
+            if((self._ready.equal(BSet())).booleanValue()):
+                self.active = BSet()
+            else:
+                self.active = BSet(pp)
+                self._ready = self._ready.difference(BSet(pp))
+
+
+    def _get_active(self):
+        return self.active
+
+    def _get__ready(self):
+        return self._ready
+
+    def _get_waiting(self):
+        return self.waiting
+
+

benchmarks/Python_Primitives/scheduler_deterministic_exec.py

+from btypes.BBoolean import BBoolean
+from btypes.BInteger import BInteger
+from btypes.BObject import BObject
+from scheduler_deterministic import scheduler_deterministic
+
+
+
+class scheduler_deterministic_exec:
+
+
+
+
+    def __init__(self):
+        self._scheduler_deterministic = scheduler_deterministic()
+
+        self.counter = BInteger(0)
+
+    def simulate(self):
+        while((self.counter.less(BInteger(200000))).booleanValue()):
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process2)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process3)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process2)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process3)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process2)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic.ready(scheduler_deterministic.PID.process2)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process3)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic.ready(scheduler_deterministic.PID.process3)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic.ready(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic.swap(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process2)
+            self._scheduler_deterministic.swap(scheduler_deterministic.PID.process3)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process2)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process2)
+            self._scheduler_deterministic.swap(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process2)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process3)
+            self._scheduler_deterministic.new(scheduler_deterministic.PID.process1)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process2)
+            self._scheduler_deterministic._del(scheduler_deterministic.PID.process1)
+            self.counter = self.counter.plus(BInteger(1))
+
+
+
+
+

benchmarks/Python_Primitives/sort_m2_data1000.py

+from btypes.BRelation import BRelation
+from btypes.BSet import BSet
+from btypes.BTuple import BTuple
+from btypes.BInteger import BInteger
+from btypes.BBoolean import BBoolean
+
+
+
+class sort_m2_data1000:
+    def __init__(self):
+        self._ic_set_0 = BRelation()
+        for _ic_i in BSet.interval(BInteger(1), BInteger(1000)):
+            self._ic_set_0 = self._ic_set_0.union(BRelation(BTuple(_ic_i, BInteger(1500).minus(_ic_i))))
+        self.f = self._ic_set_0
+        self.n = BInteger(1000)
+        self.g = self.f
+        self.k = BInteger(1)
+        self.l = BInteger(1)
+        self.j = BInteger(1)
+
+    def progress(self):
+        if BBoolean(self.k.unequal(self.n).booleanValue() and self.j.equal(self.n).booleanValue()).booleanValue():
+            _ld_g = self.g
+            _ld_k = self.k
+            _ld_l = self.l
+            self.g = _ld_g.override(BRelation(BTuple(_ld_k, _ld_g.functionCall(_ld_l))).override(BRelation(BTuple(_ld_l, _ld_g.functionCall(_ld_k)))))
+            self.k = _ld_k.plus(BInteger(1))
+            self.j = _ld_k.plus(BInteger(1))
+            self.l = _ld_k.plus(BInteger(1))
+
+    def prog1(self):
+        if (BBoolean(BBoolean(self.k.unequal(self.n).booleanValue() and
+                              self.j.unequal(self.n).booleanValue()).booleanValue() and
+                              self.g.functionCall(self.l).lessEqual(self.g.functionCall(self.j.plus(BInteger(1)))).booleanValue())).booleanValue():
+            _ld_j = self.j
+            _ld_l = self.l
+            self.l = _ld_l
+            self.j = _ld_j.plus(BInteger(1))
+
+    def prog2(self):
+        if BBoolean(BBoolean(self.k.unequal(self.n).booleanValue() and
+                             self.j.unequal(self.n).booleanValue()).booleanValue() and
+                             self.g.functionCall(self.l).greater(self.g.functionCall(self.j.plus(BInteger(1)))).booleanValue()).booleanValue():
+            _ld_j = self.j
+            self.j = _ld_j.plus(BInteger(1))
+            self.l = _ld_j.plus(BInteger(1))
+
+    def final_evt(self):
+        if (self.k.equal(self.n)).booleanValue():
+            pass

benchmarks/Python_Primitives/sort_m2_data1000_exec.py

+from btypes.BInteger import BInteger
+from sort_m2_data1000 import sort_m2_data1000
+
+class sort_m2_data1000_exec():
+
+
+    def __init__(self):
+        self._sort_m2_data1000 = sort_m2_data1000()
+        self.counter = BInteger(0)
+        self.sorted = BInteger(0)
+
+    def simulate(self):
+        while (self.sorted.less(BInteger(500))).booleanValue():
+            self.counter = BInteger(0)
+            while (self.counter.less(BInteger(999).minus(BInteger(2).multiply(self.sorted)))).booleanValue():
+                self._sort_m2_data1000.prog2()
+                self.counter = self.counter.plus(BInteger(1))
+            self.counter = BInteger(0)
+            while (self.counter.less(self.sorted)).booleanValue():
+                self._sort_m2_data1000.prog1()
+                self.counter = self.counter.plus(BInteger(1))
+            self._sort_m2_data1000.progress()
+            self.sorted = self.sorted.plus(BInteger(1))
+        while (self.sorted.less(BInteger(999))).booleanValue():
+            self.counter = BInteger(0)
+            while (self.counter.less(BInteger(999).minus(self.sorted))).booleanValue():
+                self._sort_m2_data1000.prog1()
+                self.counter = self.counter.plus(BInteger(1))
+            self._sort_m2_data1000.progress()
+            self.sorted = self.sorted.plus(BInteger(1))
+        self._sort_m2_data1000.final_evt()
+
+
+if __name__ == '__main__':
+    exec = sort_m2_data1000_exec()
+    exec.simulate()
\ No newline at end of file