Skip to content
Snippets Groups Projects
Unverified Commit 9bf0efe1 authored by Fabian Vu's avatar Fabian Vu Committed by GitHub
Browse files

Merge pull request #28 from favu100/rust-support

Rust support
parents b0f4f13a ee73cc25
Branches
No related tags found
No related merge requests found
Showing
with 8130 additions and 69 deletions
......@@ -165,4 +165,10 @@ benchmarks/execution/ProB/stdlib
/*.java
/*.mch
/*.py
**/Cargo.lock
**/vendor/
btypes_primitives/**/*.js
benchmarks/model_checking/ProB/lib
benchmarks/model_checking/ProB/stdlib
btypes_primitives/src/main/rust/bmachine/src/**
btypes_big_integer/src/main/rust/bmachine/src/**
......@@ -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,14 @@ 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
mkdir -p ./btypes_primitives/src/main/rust/bmachine/src/
mv $(DIRECTORY)/$@.rs ./btypes_primitives/src/main/rust/bmachine/src/main.rs
find $(DIRECTORY) -maxdepth 1 -type f -name "*.rs" -exec mv -v '{}' ./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:
......
......@@ -25,7 +25,7 @@ doi = {10.1007/978-3-030-34968-4_25}
The main features of B2Program are:
- Code generation from a formal model
- Code generation for model checking including parallelization, and caching (only supported in Java and C++)
- Code generation for model checking including parallelization, and caching (only supported in Java, C++ and Rust)
- Code generation of interactive domain-specific visualizations (from VisB) in HTML and JavaScript/TypeScript
......@@ -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:
......@@ -137,11 +137,11 @@ P is a conjunction of n conjuncts where the i-th conjunct must constraint xi for
### Sets:
| Set expression or predicate | Meaining |
|------------------------------|--------------------------------------------|
|-------------------------------|--------------------------------------------|
| {} | 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 |
......@@ -159,8 +159,8 @@ P is a conjunction of n conjuncts where the i-th conjunct must constraint xi for
| S /<<: T | Not Strict Subset of |
| union(S) | Generalized Union over Sets of Sets |
| inter(S) | Generalized Intersection over Sets of Sets |
| UNION(z1,...,zn).(P\|E) | Generalized Union with Predicate |
| INTER(z1,...,zn).(P\|E) | Generalized Intersection with Predicate |
| UNION(z1,...,zn).(P &#124; E) | Generalized Union with Predicate |
| INTER(z1,...,zn).(P &#124; E) | Generalized Intersection with Predicate |
Restriction: Set comprehesions, generalized unions and generalized intersections are quantified constructs. The predicate P must be a conjunction where the first n conjuncts must constraint the bounded variables.
The i-th conjunct must constraint xi for each i in {1,...,n}.
......@@ -191,8 +191,8 @@ The i-th conjunct must constraint xi for each i in {1,...,n}.
| m / n | Division |
| m ** n | Power |
| m mod n | Remainder of Division |
| PI(z1,...,zn).(P\|E) | Set product |
| SIGMA(z1,...,zn).(P\|E) | Set summation |
| PI(z1,...,zn).(P &#124; E) | Set product |
| SIGMA(z1,...,zn).(P &#124; E) | Set summation |
| succ(n) | Successor |
| pred(n) | Predecessor |
......@@ -206,22 +206,22 @@ The i-th conjunct must constraint xi for each i in {1,...,n}.
### Relations:
| Relation expression | Meaining |
|---------------------|-------------------------------------------------------|
|----------------------|-------------------------------------------------------|
| S <-> T | Set of relation |
| E \|-> F | Couple |
| E &#124;-> F | Couple |
| dom(r) | Domain of Relation |
| range(r) | Range of Relation |
| id(S) | Identity Relation |
| S <\| r | Domain Restriction |
| S <<\| r | Domain Substraction |
| r \|> S | Range Restriction |
| r \|>> S | Range Substraction |
| S <&#124; r | Domain Restriction |
| S <<&#124; r | Domain Substraction |
| r &#124;> S | Range Restriction |
| r &#124;>> S | Range Substraction |
| r~ | Inverse of Relation |
| r[S] | Relational Image |
| r1 <+ r2 | Relational Overriding |
| r1 >< r2 | Direct Product |
| (r1 ; r2) | Relational Composition |
| (r1 \|\| r2) | Parallel Product |
| (r1 &#124;&#124; r2) | Parallel Product |
| prj1(S,T) | Projection Function |
| prj2(S,T) | Projection Function |
| closure1(r) | Transitive Closure |
......@@ -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&#124;E) | Lambda Abstraction |
| f(E) | Function Application |
| f(E1,...,EN) | Function Application with Couples |
......@@ -267,8 +267,8 @@ The i-th conjunct must constraint xi for each i in {1,...,n}.
| front(S) | Front of Sequence |
| tail(S) | Tail of Sequence |
| conc(S) | Concatenation of Sequence of Sequences |
| s /\|\ n | Take first n elements of sequence |
| s \\|/ n | Drop first n elements of sequence |
| s /&#124;\ n | Take first n elements of sequence |
| s \\&#124;/ n | Drop first n elements of sequence |
The following constructs are not supported for code generation: seq(S), seq1(S), iseq(S), iseq1(S) and perm(S).
They are only allowed in the predicate of constructs for verification such as invariant or precondition.
......@@ -313,7 +313,7 @@ Restriction: STRING is a infinite set. It is only supported on the right-hand si
| x :: S | Choice from Set |
| x : (P) | Choice by Predicate |
| x <-- OP(X) | Operation Call and Assignment of Return Value |
| G \|\| H | Parallel Substitution |
| G &#124;&#124; H | Parallel Substitution |
| G ; H | Sequential Substitution |
| ANY x1,...,xn WHERE P THEN G END | Non Deterministic Choice |
| LET x1,...,xn BE x1=E1 & ... & xn = En IN G END | Let Substitution |
......@@ -367,6 +367,9 @@ Remarks:
# C
./gradlew run -Planguage="c" [-Pbig_integer="true/false" -Pminint="minint" -Pmaxint="maxint" -Pdeferred_set_size="size" -PuseConstraintSolving="true/false" -PforModelchecking="true/false"] -Pfile="<path_relative_to_project_directory>"
# Rust
./gradlew run -Planguage="rs" [-Pbig_integer="true/false" -Pminint="minint" -Pmaxint="maxint" -Pdeferred_set_size="size" -PuseConstraintSolving="true/false" -PforModelchecking="true/false"] -Pfile="<path_relative_to_project_directory>"
Default Values:
big_integer: false
minint: -2147483648
......@@ -384,7 +387,7 @@ forModelchecking: false
2. Generate code from the machine
```bash
java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l {java|cpp|python|typescript|c} [-bi <isBigInteger>] [-min <minint>] [-max <maxint>] [-dss <deferred_set_size>] [-cs <use_constraint_solving>] [-mc <for_model_checking>] [-v <visualisation] -f <file_path_relative_to_jar_file>
java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l {java|cpp|python|typescript|c|rs} [-bi <isBigInteger>] [-min <minint>] [-max <maxint>] [-dss <deferred_set_size>] [-cs <use_constraint_solving>] [-mc <for_model_checking>] [-v <visualisation] -f <file_path_relative_to_jar_file>
```
Remark: Visualisation is the path to a VisB file. It is only available for TypeScript/JavaScript
......@@ -413,6 +416,11 @@ Remark: Visualisation is the path to a VisB file. It is only available for TypeS
4. Example: `tsc --target ES6 --moduleResolution node TrafficLightExec.ts TrafficLight.ts`
(Code generated from TrafficLightExec.mch which includes TrafficLight.mch)
#### Rust
1. Copy the generated code into a cargo-project with proper dependencies set up (example: [btypes_primitives/src/main/rust/bmachine](btypes_primitives/src/main/rust/bmachine/src))
2. rename the file of the main-machine to `main.rs`
2. run `cargo build --release`
### Execute generated code (manual simulation)
......@@ -434,6 +442,10 @@ Remark: Visualisation is the path to a VisB file. It is only available for TypeS
2. `node --experimental-specifier-resolution=node <main file>`
3. Example: `node --experimental-specifier-resolution=node TrafficLightExec.js`
#### Rust
1. Write a main function in the generated main class
2. `cargo run --release`
### Execute generated model checking code
......@@ -447,6 +459,14 @@ Remark: Visualisation is the path to a VisB file. It is only available for TypeS
1. `./<main file> <strategy> <threads> <caching>`
2. Example: `./TrafficLight.exec mixed 6 true`
#### Rust
1. `cargo run --release -- <strategy> <threads> <caching> [-nodead]`
2. Example: `cargo run --release -- mixed 2 true`
Note: `threads` specifies the maximum number of executor threads. If `threads > 1`
an additional coordinator thread is created, increasing the total number of threads by one.
Remark:
* strategy : {mixed, bf, df}
......@@ -580,6 +600,25 @@ console.log(lift.getFloor().toString());
* Execute the transpiled file with `node --experimental-specifier-resolution=node Lift.js`
* Output: `3`
##### Rust
* Run `./gradlew fatJar` to build the JAR-file
* Move the built JAR-file `B2Program-all-0.1.0-SNAPSHOT` to the same directory as `Lift.mch`
* Generate code for `Lift.mch` with ```java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l rs -f Lift.mch ```
* Rename `Lift.rs` to `main.rs` and move it to [btypes_primitives/src/main/rust/bmachine/src](btypes_primitives/src/main/rust/bmachine/src)
* Write additional code executing generated functions of the Lift-machine
```rust
pub fn() {
let mut lift = Lift::new();
lift.inc();
lift.inc();
lift.inc();
println!("{}", lift.getFloor());
}
```
* from the bmachine-directory, run `cargo run --release`
* Output: `3`
#### Model Checking
##### Java
......@@ -608,6 +647,15 @@ make install
* Execute `Lift.exec` with `./Lift 1 false`
##### Rust
* Run `./gradlew fatJar` to build the JAR-file
* Move the built JAR-file `B2Program-all-0.1.0-SNAPSHOT` to the same folder as `Lift.mch`
* Generate code for `Lift.mch` with ```java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l rs -f Lift.mch -mc true```
* Rename `Lift.rs` to `main.rs` and move it to [btypes_primitives/src/main/rust/bmachine/src](btypes_primitives/src/main/rust/bmachine/src)
* from the bmachine-directory, run `cargo run --release -- mixed 1 false`
### Example 2: Cruise_finite1_deterministic_exec
The file for `Cruise_finite1_deterministic_exec.mch` and `Cruise_finite1_deterministic` are in https://github.com/favu100/b2program/tree/master/src/test/resources/de/hhu/stups/codegenerator.
The machine Cruise_finite1_deterministic_exec includes the machine Cruise_finite1_deterministic.
......@@ -767,6 +815,52 @@ false
false
```
##### Rust
* Run `./gradlew fatJar` to build the JAR-file
* Move the built JAR-file `B2Program-all-0.1.0-SNAPSHOT` to the same folder as `Cruise_finite1_deterministic_exec.mch` and `Cruise_finite1_deterministic.mch`
* Generate code for `Cruise_finite1_deterministic_exec.mch` ```java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l rs -f Cruise_finite1_deterministic.mch```
* Rename `Cruise_finite1_deterministic_exec.rs` to `main.rs` and move it and `Cruise_finite1_deterministic.rs` to [btypes_primitives/src/main/rust/bmachine/src](btypes_primitives/src/main/rust/bmachine/src)
* Write additional code in `main.rs`
```rust
pub fn() {
let mut cruise = Cruise_finite1_deterministic_exec::new();
cruise.simulate();
println!("{}", cruise._Cruise_finite1_deterministic._get_CruiseAllowed());
println!("{}", cruise._Cruise_finite1_deterministic._get_CruiseActive());
println!("{}", cruise._Cruise_finite1_deterministic._get_VehicleAtCruiseSpeed());
println!("{}", cruise._Cruise_finite1_deterministic._get_VehicleCanKeepSpeed());
println!("{}", cruise._Cruise_finite1_deterministic._get_VehicleTryKeepSpeed());
println!("{}", cruise._Cruise_finite1_deterministic._get_SpeedAboveMax());
println!("{}", cruise._Cruise_finite1_deterministic._get_VehicleTryKeepTimeGap());
println!("{}", cruise._Cruise_finite1_deterministic._get_CruiseSpeedAtMax());
println!("{}", cruise._Cruise_finite1_deterministic._get_ObstaclePresent());
println!("{}", cruise._Cruise_finite1_deterministic._get_ObstacleDistance());
println!("{}", cruise._Cruise_finite1_deterministic._get_ObstacleRelativeSpeed());
println!("{}", cruise._Cruise_finite1_deterministic._get_ObstacleStatusJustChanged());
println!("{}", cruise._Cruise_finite1_deterministic._get_CCInitialisationInProgress());
println!("{}", cruise._Cruise_finite1_deterministic._get_CruiseSpeedChangeInProgress());
}
```
* from the bmachine-directory, run `cargo run --release`
* Output:
```bash
false
false
false
false
false
false
false
false
false
ODnone
RSnone
false
false
false
```
#### Model Checking
##### Java
......@@ -793,3 +887,12 @@ make install
* Compile `Cruise_finite1_deterministic.cpp` with `g++ -std=c++14 -O2 -flto -march=native -g -DIMMER_NO_THREAD_SAFETY -o Cruise_finite1_deterministic.exec Cruise_finite1_deterministic.cpp`
* Execute `Cruise_finite1_deterministic.exec` with `./Cruise_finite1_deterministic.exec mixed 6 true`
##### Rust
* Run `./gradlew fatJar` to build the JAR-file
* Move the built JAR-file `B2Program-all-0.1.0-SNAPSHOT` to the same folder as `Cruise_finite1_deterministic.mch` and `Cruise_finite1_deterministic.mch`
* Generate code for `Cruise_finite1_deterministic.mch` `java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l rs -f Cruise_finite1_deterministic.mch -mc true`
* Rename `Cruise_finite1_deterministic_exec.rs` to `main.rs` and move it and `Cruise_finite1_deterministic.rs` to [btypes_primitives/src/main/rust/bmachine/src](btypes_primitives/src/main/rust/bmachine/src)
* from the bmachine-directory, run `cargo run --release -- mixed 6 true`
\ No newline at end of file
import statistics
import sys
from datetime import timedelta
file = sys.argv[1]
print('opening file: ', file)
full_print = True
mc = True
for arg in sys.argv[2:]:
if arg.upper() == 'SHORT':
full_print = False
elif arg.upper() == 'NO_MC':
mc = False
# {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 = ('', '', 1, 'False', 0, '')
if mc:
machine, mode, threads, caching, time, memory = stripped_line.split(' ')
else:
machine, time, memory = stripped_line.split(' ')
if machine not in data:
data[machine] = {}
params = (mode, int(threads), caching.upper() == '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
parsed_times = []
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)
parsed_time = timedelta(minutes=minutes, seconds=seconds, milliseconds=millis)
avg_time += parsed_time
parsed_times += [parsed_time]
parsed_times.sort()
if number_of_datapoints <= 0:
continue
avg_time /= number_of_datapoints
median_time = parsed_times[len(parsed_times) // 2]
if len(parsed_times) % 2 == 0:
median_time = (median_time + parsed_times[len(parsed_times) // 2 + 1]) / 2
memories = data[machine][params]['memory']
memories.sort()
median_memory = memories[len(memories) // 2]
if len(memories) % 2 == 0:
median_memory = (median_memory + memories[len(memories) // 2 + 1]) / 2
spacing = " "*(len(machine) + len(params[0]) + len(str(params[1])) + len(str(params[2])) - 5)
print(f'{machine} {params[0]} {params[1]} {params[2]} {round(median_time.total_seconds(), 2)} {round(median_memory)}')
if full_print:
print( f'{spacing}time : min {round(parsed_times[0].total_seconds(), 2)}, '
f'median: {round(median_time.total_seconds(), 2)}, '
f'average: {round(avg_time.total_seconds(), 2)}, '
f'max: {round(parsed_times[-1].total_seconds(), 2)}')
print( f'{spacing}memory: min {round(memories[0])}, '
f'median: {round(median_memory)}, '
f'average: {round(statistics.fmean(memories))}, '
f'max: {round(memories[-1])}')
......@@ -40,6 +40,39 @@ Executing benchmarks is done by executing ``make`` in each of the directories.
| | **Speedup** | 1 | > 84.67 | > 117.96 | > 151.26 | > 6000 |
| | **Memory** | - | 750 816 | 484 948 | 864 | 820 |
## Results (Rust)
Rust development was done on a different system, therefore benchmarks are not comparable to the old table.
These benchmarks where run on a Ryzen 7 1700 under Debian via wsl (Win 10)
(Memory values seem pretty high. GNU time had a bug for reporting 4x the RSS, but I'm using version 1.9 here,
which apparently has it fixed...)
| Machines | | ProB | Java PI | Java BI | C++ PI -O1 | C++ PI -O2 | Rust PI O1 | Rust PI O2 | Rust PI O3 | Rust BI O2 | Rust BI O3 |
|-------------------|-------------|------------|-----------|-----------|------------|------------|------------|------------|------------|------------|------------|
| Lift | **Runtime** | > 1200 | 11.85 | 102.67 | 51.05 | 00.00 | 20.55 | 18.43 | 18.49 | 685.03 | 705.46 |
| | **Speedup** | | | | | | | | | | |
| | **Memory** | - | 2 220 976 | 2 247 676 | 3120 | 3060 | 2160 | 2276 | 2168 | 2572 | 2584 |
| TrafficLight | **Runtime** | > 1200 | 05.21 | 17.40 | 51.35 | 00.00 | 21.31 | 10.87 | 10.78 | 78.33 | 80.27 |
| | **Speedup** | | | | | | | | | | |
| | **Memory** | - | 1 400 352 | 2 202 788 | 3188 | 3188 | 2312 | 2256 | 2312 | 2496 | 2664 |
| Sieve | **Runtime** | 83.76 | 07.41 | 08.04 | 26.15 | 06.86 | 53.04 | 09.03 | 09.06 | 39.27 | 39.54 |
| | **Speedup** | 1 | 11.3 | 10.42 | 3.2 | 12.2 | 1.58 | 9.28 | 9.25 | 2.13 | 2.12 |
| | **Memory** | 414 232 | 2 094 128 | 2 079 056 | 165 528 | 165 548 | 104 764 | 104 608 | 104 604 | 450 804 | 450 688 |
| Scheduler | **Runtime** | 429.98 | 06.39 | 06.39 | 14.25 | 01.98 | 34.97 | 06.14 | 06.04 | 06.28 | 06.00 |
| | **Speedup** | 1 | 67.29 | 67.29 | 30.17 | 217.16 | 12.3 | 70.03 | 71.19 | 68.47 | 71.66 |
| | **Memory** | 14 738 152 | 1 422 120 | 1 415 844 | 3080 | 3136 | 2384 | 2228 | 2324 | 2528 | 2584 |
| sort_m2_data1000 | **Runtime** | 18.99 | 02.02 | 02.15 | 00.20 | 00.03 | 02.77 | 00.50 | 00.51 | 01.11 | 01.15 |
| | **Speedup** | 1 | 9.4 | 8.83 | 94.95 | 633 | 6.86 | 37.98 | 37.24 | 17.11 | 16.51 |
| | **Memory** | 594 428 | 204 220 | 206 676 | 3412 | 3420 | 5312 | 5216 | 5328 | 10072 | 9872 |
| CAN Bus | **Runtime** | 310.92 | 05.17 | 05.15 | 05.80 | 00.59 | 19.83 | 03.16 | 03.18 | 06.36 | 06.47 |
| | **Speedup** | 1 | 60.14 | 60.37 | 53.61 | 526.98 | 15.68 | 98.39 | 97.77 | 48.89 | 48.06 |
| | **Memory** | 184 356 | 930 816 | 917 552 | 3364 | 3208 | 2668 | 2540 | 2508 | 2912 | 2928 |
| Train | **Runtime** | 66.66 | 07.40 | 07.57 | 13.19 | 01.64 | 31.52 | 04.76 | 04.71 | 02.78 | 02.77 |
| | **Speedup** | 1 | 9.01 | 8.81 | 5.05 | 40.65 | 2.11 | 14 | 14.15 | 23.98 | 24.06 |
| | **Memory** | 179 880 | 1 420 528 | 1419832 | 3224 | 3372 | 2740 | 2636 | 2612 | 2856 | 2812 |
| Cruise Controller | **Runtime** | > 1200 | 13.91 | 14.66 | 08.34 | 00.04 | 05.15 | 05.43 | 05.33 | 14.20 | 14.64 |
| | **Speedup** | | | | | | | | | | |
| | **Memory** | - | 1 401 192 | 1 400 232 | 3160 | 3092 | 2376 | 2540 | 2352 | 2668 | 2668 |
Runtime in Seconds
Memory Usage in KB
......
#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
use btypes::bboolean::BBoolean;
use btypes::binteger::BInteger;
use btypes::brelation::BRelation;
use btypes::bset::BSet;
use btypes::bobject::BObject;
use btypes::btuple::BTuple;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T1state {
T1_EN,
T1_CALC,
T1_SEND,
T1_WAIT
}
impl T1state {
pub fn equal(&self, other: &T1state) -> BBoolean { BBoolean::new(*self == *other)}
pub fn unequal(&self, other: &T1state) -> BBoolean { BBoolean::new(*self != *other)}
}
impl BObject for T1state {}
impl Default for T1state {
fn default() -> Self { T1state::T1_EN }
}
impl fmt::Display for T1state {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match *self {
T1state::T1_EN => write!(f, "T1_EN"),
T1state::T1_CALC => write!(f, "T1_CALC"),
T1state::T1_SEND => write!(f, "T1_SEND"),
T1state::T1_WAIT => write!(f, "T1_WAIT"),
}
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T2mode {
T2MODE_SENSE,
T2MODE_TRANSMIT,
T2MODE_RELEASE
}
impl T2mode {
pub fn equal(&self, other: &T2mode) -> BBoolean { BBoolean::new(*self == *other)}
pub fn unequal(&self, other: &T2mode) -> BBoolean { BBoolean::new(*self != *other)}
}
impl BObject for T2mode {}
impl Default for T2mode {
fn default() -> Self { T2mode::T2MODE_SENSE }
}
impl fmt::Display for T2mode {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match *self {
T2mode::T2MODE_SENSE => write!(f, "T2MODE_SENSE"),
T2mode::T2MODE_TRANSMIT => write!(f, "T2MODE_TRANSMIT"),
T2mode::T2MODE_RELEASE => write!(f, "T2MODE_RELEASE"),
}
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T2state {
T2_EN,
T2_RCV,
T2_PROC,
T2_CALC,
T2_SEND,
T2_WAIT,
T2_RELEASE
}
impl T2state {
pub fn equal(&self, other: &T2state) -> BBoolean { BBoolean::new(*self == *other)}
pub fn unequal(&self, other: &T2state) -> BBoolean { BBoolean::new(*self != *other)}
}
impl BObject for T2state {}
impl Default for T2state {
fn default() -> Self { T2state::T2_EN }
}
impl fmt::Display for T2state {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match *self {
T2state::T2_EN => write!(f, "T2_EN"),
T2state::T2_RCV => write!(f, "T2_RCV"),
T2state::T2_PROC => write!(f, "T2_PROC"),
T2state::T2_CALC => write!(f, "T2_CALC"),
T2state::T2_SEND => write!(f, "T2_SEND"),
T2state::T2_WAIT => write!(f, "T2_WAIT"),
T2state::T2_RELEASE => write!(f, "T2_RELEASE"),
}
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum T3state {
T3_READY,
T3_WRITE,
T3_RELEASE,
T3_READ,
T3_PROC,
T3_WAIT
}
impl T3state {
pub fn equal(&self, other: &T3state) -> BBoolean { BBoolean::new(*self == *other)}
pub fn unequal(&self, other: &T3state) -> BBoolean { BBoolean::new(*self != *other)}
}
impl BObject for T3state {}
impl Default for T3state {
fn default() -> Self { T3state::T3_READY }
}
impl fmt::Display for T3state {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match *self {
T3state::T3_READY => write!(f, "T3_READY"),
T3state::T3_WRITE => write!(f, "T3_WRITE"),
T3state::T3_RELEASE => write!(f, "T3_RELEASE"),
T3state::T3_READ => write!(f, "T3_READ"),
T3state::T3_PROC => write!(f, "T3_PROC"),
T3state::T3_WAIT => write!(f, "T3_WAIT"),
}
}
}
#[derive(Default, Debug)]
pub struct CAN_BUS_tlc {
BUSpriority: BInteger,
BUSvalue: BInteger,
BUSwrite: BRelation<BInteger, BInteger>,
T1_state: T1state,
T1_timer: BInteger,
T1_writevalue: BInteger,
T2_mode: T2mode,
T2_readpriority: BInteger,
T2_readvalue: BInteger,
T2_state: T2state,
T2_timer: BInteger,
T2_writevalue: BInteger,
T2v: BInteger,
T3_enabled: BBoolean,
T3_evaluated: BBoolean,
T3_readpriority: BInteger,
T3_readvalue: BInteger,
T3_state: T3state,
NATSET: BSet<BInteger>,
_T1state: BSet<T1state>,
_T2mode: BSet<T2mode>,
_T2state: BSet<T2state>,
_T3state: BSet<T3state>,
}
impl CAN_BUS_tlc {
pub fn new() -> CAN_BUS_tlc {
//values: ''
let mut m: CAN_BUS_tlc = Default::default();
m.init();
return m;
}
fn init(&mut self) {
self.NATSET = BSet::<BInteger>::interval(&BInteger::new(b"0"), &BInteger::new(b"5"));
self._T1state = BSet::new(vec![T1state::T1_EN, T1state::T1_CALC, T1state::T1_SEND, T1state::T1_WAIT]);
self._T2mode = BSet::new(vec![T2mode::T2MODE_SENSE, T2mode::T2MODE_TRANSMIT, T2mode::T2MODE_RELEASE]);
self._T2state = BSet::new(vec![T2state::T2_EN, T2state::T2_RCV, T2state::T2_PROC, T2state::T2_CALC, T2state::T2_SEND, T2state::T2_WAIT, T2state::T2_RELEASE]);
self._T3state = BSet::new(vec![T3state::T3_READY, T3state::T3_WRITE, T3state::T3_RELEASE, T3state::T3_READ, T3state::T3_PROC, T3state::T3_WAIT]);
self.T2v = BInteger::new(b"0").clone();
self.T3_evaluated = BBoolean::new(true).clone();
self.T3_enabled = BBoolean::new(true).clone();
self.T1_state = T1state::T1_EN.clone();
self.T2_state = T2state::T2_EN.clone();
self.T3_state = T3state::T3_READY.clone();
self.T1_writevalue = BInteger::new(b"0").clone();
self.T2_writevalue = BInteger::new(b"0").clone();
self.T2_readvalue = BInteger::new(b"0").clone();
self.T2_readpriority = BInteger::new(b"0").clone();
self.T3_readvalue = BInteger::new(b"0").clone();
self.T3_readpriority = BInteger::new(b"0").clone();
self.T1_timer = BInteger::new(b"2").clone();
self.T2_timer = BInteger::new(b"3").clone();
self.BUSwrite = BRelation::new(vec![BTuple::from_refs(&BInteger::new(b"0"), &BInteger::new(b"0"))]).clone().clone();
self.BUSvalue = BInteger::new(b"0").clone();
self.BUSpriority = BInteger::new(b"0").clone();
self.T2_mode = T2mode::T2MODE_SENSE.clone();
}
pub fn get_NATSET(&self) -> BSet<BInteger> {
return self.NATSET.clone();
}
pub fn get_BUSpriority(&self) -> BInteger {
return self.BUSpriority.clone();
}
pub fn get_BUSvalue(&self) -> BInteger {
return self.BUSvalue.clone();
}
pub fn get_BUSwrite(&self) -> BRelation<BInteger, BInteger> {
return self.BUSwrite.clone();
}
pub fn get_T1_state(&self) -> T1state {
return self.T1_state.clone();
}
pub fn get_T1_timer(&self) -> BInteger {
return self.T1_timer.clone();
}
pub fn get_T1_writevalue(&self) -> BInteger {
return self.T1_writevalue.clone();
}
pub fn get_T2_mode(&self) -> T2mode {
return self.T2_mode.clone();
}
pub fn get_T2_readpriority(&self) -> BInteger {
return self.T2_readpriority.clone();
}
pub fn get_T2_readvalue(&self) -> BInteger {
return self.T2_readvalue.clone();
}
pub fn get_T2_state(&self) -> T2state {
return self.T2_state.clone();
}
pub fn get_T2_timer(&self) -> BInteger {
return self.T2_timer.clone();
}
pub fn get_T2_writevalue(&self) -> BInteger {
return self.T2_writevalue.clone();
}
pub fn get_T2v(&self) -> BInteger {
return self.T2v.clone();
}
pub fn get_T3_enabled(&self) -> BBoolean {
return self.T3_enabled.clone();
}
pub fn get_T3_evaluated(&self) -> BBoolean {
return self.T3_evaluated.clone();
}
pub fn get_T3_readpriority(&self) -> BInteger {
return self.T3_readpriority.clone();
}
pub fn get_T3_readvalue(&self) -> BInteger {
return self.T3_readvalue.clone();
}
pub fn get_T3_state(&self) -> T3state {
return self.T3_state.clone();
}
pub fn get__T1state(&self) -> BSet<T1state> {
return self._T1state.clone();
}
pub fn get__T2mode(&self) -> BSet<T2mode> {
return self._T2mode.clone();
}
pub fn get__T2state(&self) -> BSet<T2state> {
return self._T2state.clone();
}
pub fn get__T3state(&self) -> BSet<T3state> {
return self._T3state.clone();
}
pub fn T1Evaluate(&mut self) -> () {
self.T1_timer = BInteger::new(b"0").clone();
self.T1_state = T1state::T1_CALC.clone();
}
pub fn T1Calculate(&mut self, mut p: BInteger) -> () {
self.T1_writevalue = p.clone();
self.T1_state = T1state::T1_SEND.clone();
}
pub fn T1SendResult(&mut self, mut ppriority: BInteger, mut pv: BInteger) -> () {
let mut _ld_BUSwrite = self.BUSwrite.clone();
self.BUSwrite = _ld_BUSwrite._override(&BRelation::new(vec![BTuple::from_refs(&ppriority, &pv)])).clone().clone();
self.T1_state = T1state::T1_WAIT.clone();
}
pub fn T1Wait(&mut self, mut pt: BInteger) -> () {
self.T1_timer = pt.clone();
self.T1_state = T1state::T1_EN.clone();
}
pub fn T2Evaluate(&mut self) -> () {
self.T2_timer = BInteger::new(b"0").clone();
self.T2_state = T2state::T2_RCV.clone();
}
pub fn T2ReadBus(&mut self, mut ppriority: BInteger, mut pv: BInteger) -> () {
self.T2_readvalue = pv.clone();
self.T2_readpriority = ppriority.clone();
self.T2_state = T2state::T2_PROC.clone();
}
pub fn T2Reset(&mut self) -> () {
let mut _ld_T2v = self.T2v.clone();
self.T2_writevalue = _ld_T2v.clone();
self.T2v = BInteger::new(b"0").clone();
self.T2_state = T2state::T2_SEND.clone();
self.T2_mode = T2mode::T2MODE_TRANSMIT.clone();
}
pub fn T2Complete(&mut self) -> () {
self.T2_state = T2state::T2_RELEASE.clone();
self.T2_mode = T2mode::T2MODE_SENSE.clone();
}
pub fn T2ReleaseBus(&mut self, mut ppriority: BInteger) -> () {
let mut _ld_BUSwrite = self.BUSwrite.clone();
self.BUSwrite = _ld_BUSwrite.domainSubstraction(&BSet::new(vec![ppriority])).clone().clone();
self.T2_state = T2state::T2_WAIT.clone();
}
pub fn T2Calculate(&mut self) -> () {
self.T2v = self.T2_readvalue.clone();
self.T2_state = T2state::T2_WAIT.clone();
}
pub fn T2WriteBus(&mut self, mut ppriority: BInteger, mut pv: BInteger) -> () {
let mut _ld_BUSwrite = self.BUSwrite.clone();
self.BUSwrite = _ld_BUSwrite._override(&BRelation::new(vec![BTuple::from_refs(&ppriority, &pv)])).clone().clone();
self.T2_state = T2state::T2_WAIT.clone();
}
pub fn T2Wait(&mut self, mut pt: BInteger) -> () {
self.T2_timer = pt.clone();
self.T2_state = T2state::T2_EN.clone();
}
pub fn T3Initiate(&mut self) -> () {
self.T3_state = T3state::T3_WRITE.clone();
self.T3_enabled = BBoolean::new(false).clone();
}
pub fn T3Evaluate(&mut self) -> () {
self.T3_state = T3state::T3_READ.clone();
}
pub fn T3writebus(&mut self, mut ppriority: BInteger, mut pv: BInteger) -> () {
let mut _ld_BUSwrite = self.BUSwrite.clone();
self.BUSwrite = _ld_BUSwrite._override(&BRelation::new(vec![BTuple::from_refs(&ppriority, &pv)])).clone().clone();
self.T3_state = T3state::T3_WAIT.clone();
}
pub fn T3Read(&mut self, mut ppriority: BInteger, mut pv: BInteger) -> () {
self.T3_readvalue = pv.clone();
self.T3_readpriority = ppriority.clone();
self.T3_state = T3state::T3_PROC.clone();
}
pub fn T3Poll(&mut self) -> () {
self.T3_state = T3state::T3_WAIT.clone();
}
pub fn T3ReleaseBus(&mut self, mut ppriority: BInteger) -> () {
let mut _ld_BUSwrite = self.BUSwrite.clone();
self.BUSwrite = _ld_BUSwrite.domainSubstraction(&BSet::new(vec![ppriority])).clone().clone();
self.T3_state = T3state::T3_RELEASE.clone();
}
pub fn T3Wait(&mut self) -> () {
self.T3_state = T3state::T3_READY.clone();
self.T3_evaluated = BBoolean::new(true).clone();
}
pub fn T3ReEnableWait(&mut self) -> () {
self.T3_state = T3state::T3_READY.clone();
self.T3_evaluated = BBoolean::new(true).clone();
self.T3_enabled = BBoolean::new(true).clone();
}
pub fn Update(&mut self, mut pmax: BInteger) -> () {
let mut _ld_T1_timer = self.T1_timer.clone();
let mut _ld_T2_timer = self.T2_timer.clone();
self.BUSvalue = self.BUSwrite.functionCall(&pmax).clone();
self.BUSpriority = pmax.clone();
self.T1_timer = _ld_T1_timer.minus(&BInteger::new(b"1")).clone();
self.T2_timer = _ld_T2_timer.minus(&BInteger::new(b"1")).clone();
self.T3_evaluated = BBoolean::new(false).clone();
}
}
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
use btypes::binteger::BInteger;
#[derive(Default, Debug)]
pub struct Lift {
floor: BInteger,
}
impl Lift {
pub fn new() -> Lift {
//values: ''
let mut m: Lift = Default::default();
m.init();
return m;
}
fn init(&mut self) {
self.floor = BInteger::new(b"0");
}
pub fn get_floor(&self) -> BInteger {
return self.floor.clone();
}
pub fn inc(&mut self) -> () {
self.floor = self.floor.plus(&BInteger::new(b"1"));
}
pub fn dec(&mut self) -> () {
self.floor = self.floor.minus(&BInteger::new(b"1"));
}
}
#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
use btypes::binteger::BInteger;
use btypes::bboolean::BBoolean;
mod Lift;
#[derive(Default, Debug)]
pub struct LiftExec {
counter: BInteger,
_Lift: Lift::Lift,
}
impl LiftExec {
pub fn new() -> LiftExec {
//values: ''
let mut m: LiftExec = Default::default();
m.init();
return m;
}
fn init(&mut self) {
self.counter = BInteger::new(b"0");
self._Lift = Lift::Lift::new();
}
pub fn get_counter(&self) -> BInteger {
return self.counter.clone();
}
pub fn simulate(&mut self) -> () {
while (self.counter.less(&BInteger::new(b"10000000"))).booleanValue() {
let mut i: Option<BInteger> = Option::None;
i = Option::Some(BInteger::new(b"0"));
while (i.as_ref().unwrap().less(&BInteger::new(b"100"))).booleanValue() {
self._Lift.inc();
i = Option::Some(i.as_ref().unwrap().plus(&BInteger::new(b"1")));
}
let mut _i: Option<BInteger> = Option::None;
_i = Option::Some(BInteger::new(b"0"));
while (_i.as_ref().unwrap().less(&BInteger::new(b"100"))).booleanValue() {
self._Lift.dec();
_i = Option::Some(_i.as_ref().unwrap().plus(&BInteger::new(b"1")));
}
self.counter = self.counter.plus(&BInteger::new(b"1"));
}
}
}
fn main() {
let mut exec = LiftExec::new();
exec.simulate();
}
.SUFFIXES:
.PHONY: all clean
all: CAN_BUS_tlc_exec Cruise_finite1_deterministic_exec LiftExec scheduler_deterministic_exec Sieve_exec Train_1_beebook_deterministic_exec TrafficLightExec sort_m2_data1000_exec
OUTPUT ?= runtimes.txt
CARGO_PROJ_PATH=../../../btypes_big_integer/src/main/rust/bmachine
CARGO_BUILD=cargo build --release --manifest-path $(CARGO_PROJ_PATH)/Cargo.toml
%.main : %.rs
cp $(*).rs $(CARGO_PROJ_PATH)/src/$(*).rs
%Exec.cp : %Exec.rs %.main
cp $(*)Exec.rs $(CARGO_PROJ_PATH)/src/main.rs
%_exec.cp : %_exec.rs %.main
cp $(*)_exec.rs $(CARGO_PROJ_PATH)/src/main.rs
% : clean %.cp
$(CARGO_BUILD)
/usr/bin/time -f "$(*) %E %M" -ao $(OUTPUT) $(CARGO_PROJ_PATH)/target/release/bmachine
clean:
rm -f $(CARGO_PROJ_PATH)/src/*.rs
\ No newline at end of file
#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
use btypes::binteger::BInteger;
use btypes::bboolean::BBoolean;
use btypes::bset::BSet;
#[derive(Default, Debug)]
pub struct Sieve {
numbers: BSet<BInteger>,
cur: BInteger,
limit: BInteger,
}
impl Sieve {
pub fn new() -> Sieve {
//values: ''
let mut m: Sieve = Default::default();
m.init();
return m;
}
fn init(&mut self) {
self.numbers = BSet::<BInteger>::interval(&BInteger::new(b"2"), &BInteger::new(b"2000000")).clone().clone();
self.cur = BInteger::new(b"2").clone();
self.limit = BInteger::new(b"2000000").clone();
}
pub fn get_numbers(&self) -> BSet<BInteger> {
return self.numbers.clone();
}
pub fn get_cur(&self) -> BInteger {
return self.cur.clone();
}
pub fn get_limit(&self) -> BInteger {
return self.limit.clone();
}
pub fn ComputeNumberOfPrimes(&mut self) -> BInteger {
let mut res: Option<BInteger> = Option::None;
while (self.cur.greater(&BInteger::new(b"1")).and(&self.cur.multiply(&self.cur).lessEqual(&self.limit))).booleanValue() {
if (self.numbers.elementOf(&self.cur)).booleanValue() {
let mut n: Option<BInteger> = Option::None;
let mut set: Option<BSet<BInteger>> = Option::None;
n = Option::Some(self.cur.clone());
set = Option::Some(BSet::new(vec![]).clone()).clone();
while (n.as_ref().unwrap().lessEqual(&self.limit.divide(&self.cur))).booleanValue() {
set = Option::Some(set.as_ref().unwrap()._union(&BSet::new(vec![self.cur.multiply(&n.as_ref().unwrap())])).clone()).clone();
n = Option::Some(n.as_ref().unwrap().plus(&BInteger::new(b"1")).clone());
}
self.numbers = self.numbers.difference(&set.as_ref().unwrap()).clone().clone();
}
self.cur = self.cur.plus(&BInteger::new(b"1")).clone();
}
res = Option::Some(self.numbers.card().clone());
return res.unwrap();
}
}
mod Sieve;
fn main(){
let mut sieve = Sieve::Sieve::new();
println!("{}", sieve.ComputeNumberOfPrimes());
}
\ No newline at end of file
#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
use btypes::bboolean::BBoolean;
use btypes::bset::BSet;
use btypes::bobject::BObject;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum colors {
red,
redyellow,
yellow,
green
}
impl colors {
pub fn equal(&self, other: &colors) -> BBoolean { BBoolean::new(*self == *other)}
pub fn unequal(&self, other: &colors) -> BBoolean { BBoolean::new(*self != *other)}
}
impl BObject for colors {}
impl Default for colors {
fn default() -> Self { colors::red }
}
impl fmt::Display for colors {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match *self {
colors::red => write!(f, "red"),
colors::redyellow => write!(f, "redyellow"),
colors::yellow => write!(f, "yellow"),
colors::green => write!(f, "green"),
}
}
}
#[derive(Default, Debug)]
pub struct TrafficLight {
tl_cars: colors,
tl_peds: colors,
_colors: BSet<colors>,
}
impl TrafficLight {
pub fn new() -> TrafficLight {
//values: ''
let mut m: TrafficLight = Default::default();
m.init();
return m;
}
fn init(&mut self) {
self._colors = BSet::new(vec![colors::red, colors::redyellow, colors::yellow, colors::green]);
self.tl_cars = colors::red;
self.tl_peds = colors::red;
}
pub fn get_tl_cars(&self) -> colors {
return self.tl_cars.clone();
}
pub fn get_tl_peds(&self) -> colors {
return self.tl_peds.clone();
}
pub fn get__colors(&self) -> BSet<colors> {
return self._colors.clone();
}
pub fn cars_ry(&mut self) -> () {
if (self.tl_cars.equal(&colors::red).and(&self.tl_peds.equal(&colors::red))).booleanValue() {
self.tl_cars = colors::redyellow;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
pub fn cars_y(&mut self) -> () {
if (self.tl_cars.equal(&colors::green).and(&self.tl_peds.equal(&colors::red))).booleanValue() {
self.tl_cars = colors::yellow;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
pub fn cars_g(&mut self) -> () {
if (self.tl_cars.equal(&colors::redyellow).and(&self.tl_peds.equal(&colors::red))).booleanValue() {
self.tl_cars = colors::green;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
pub fn cars_r(&mut self) -> () {
if (self.tl_cars.equal(&colors::yellow).and(&self.tl_peds.equal(&colors::red))).booleanValue() {
self.tl_cars = colors::red;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
pub fn peds_r(&mut self) -> () {
if (self.tl_peds.equal(&colors::green).and(&self.tl_cars.equal(&colors::red))).booleanValue() {
self.tl_peds = colors::red;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
pub fn peds_g(&mut self) -> () {
if (self.tl_peds.equal(&colors::red).and(&self.tl_cars.equal(&colors::red))).booleanValue() {
self.tl_peds = colors::green;
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
}
#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
use btypes::binteger::BInteger;
use btypes::bboolean::BBoolean;
mod TrafficLight;
#[derive(Default, Debug)]
pub struct TrafficLightExec {
counter: BInteger,
_TrafficLight: TrafficLight::TrafficLight,
}
impl TrafficLightExec {
pub fn new() -> TrafficLightExec {
//values: ''
let mut m: TrafficLightExec = Default::default();
m.init();
return m;
}
fn init(&mut self) {
self.counter = BInteger::new(b"0");
self._TrafficLight = TrafficLight::TrafficLight::new();
}
pub fn get_counter(&self) -> BInteger {
return self.counter.clone();
}
pub fn simulate(&mut self) -> () {
while (self.counter.less(&BInteger::new(b"300000000"))).booleanValue() {
self._TrafficLight.cars_ry();
self._TrafficLight.cars_g();
self._TrafficLight.cars_y();
self._TrafficLight.cars_r();
self._TrafficLight.peds_g();
self._TrafficLight.peds_r();
self.counter = self.counter.plus(&BInteger::new(b"1"));
}
}
}
fn main() {
let mut exec = TrafficLightExec::new();
exec.simulate();
}
#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
use btypes::bboolean::BBoolean;
use btypes::brelation::BRelation;
use btypes::bset::BSet;
use btypes::bobject::BObject;
use btypes::btuple::BTuple;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum BLOCKS {
A,
B,
C,
D,
E,
F,
G,
H,
I,
J,
K,
L,
M,
N
}
impl BLOCKS {
pub fn equal(&self, other: &BLOCKS) -> BBoolean { BBoolean::new(*self == *other)}
pub fn unequal(&self, other: &BLOCKS) -> BBoolean { BBoolean::new(*self != *other)}
}
impl BObject for BLOCKS {}
impl Default for BLOCKS {
fn default() -> Self { BLOCKS::A }
}
impl fmt::Display for BLOCKS {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match *self {
BLOCKS::A => write!(f, "A"),
BLOCKS::B => write!(f, "B"),
BLOCKS::C => write!(f, "C"),
BLOCKS::D => write!(f, "D"),
BLOCKS::E => write!(f, "E"),
BLOCKS::F => write!(f, "F"),
BLOCKS::G => write!(f, "G"),
BLOCKS::H => write!(f, "H"),
BLOCKS::I => write!(f, "I"),
BLOCKS::J => write!(f, "J"),
BLOCKS::K => write!(f, "K"),
BLOCKS::L => write!(f, "L"),
BLOCKS::M => write!(f, "M"),
BLOCKS::N => write!(f, "N"),
}
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum ROUTES {
R1,
R2,
R3,
R4,
R5,
R6,
R7,
R8,
R9,
R10
}
impl ROUTES {
pub fn equal(&self, other: &ROUTES) -> BBoolean { BBoolean::new(*self == *other)}
pub fn unequal(&self, other: &ROUTES) -> BBoolean { BBoolean::new(*self != *other)}
}
impl BObject for ROUTES {}
impl Default for ROUTES {
fn default() -> Self { ROUTES::R1 }
}
impl fmt::Display for ROUTES {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match *self {
ROUTES::R1 => write!(f, "R1"),
ROUTES::R2 => write!(f, "R2"),
ROUTES::R3 => write!(f, "R3"),
ROUTES::R4 => write!(f, "R4"),
ROUTES::R5 => write!(f, "R5"),
ROUTES::R6 => write!(f, "R6"),
ROUTES::R7 => write!(f, "R7"),
ROUTES::R8 => write!(f, "R8"),
ROUTES::R9 => write!(f, "R9"),
ROUTES::R10 => write!(f, "R10"),
}
}
}
#[derive(Default, Debug)]
pub struct Train_1_beebook_deterministic {
LBT: BSet<BLOCKS>,
TRK: BRelation<BLOCKS, BLOCKS>,
frm: BSet<ROUTES>,
OCC: BSet<BLOCKS>,
resbl: BSet<BLOCKS>,
resrt: BSet<ROUTES>,
rsrtbl: BRelation<BLOCKS, ROUTES>,
fst: BRelation<ROUTES, BLOCKS>,
lst: BRelation<ROUTES, BLOCKS>,
nxt: BRelation<ROUTES, BRelation<BLOCKS, BLOCKS>>,
rtbl: BRelation<BLOCKS, ROUTES>,
_BLOCKS: BSet<BLOCKS>,
_ROUTES: BSet<ROUTES>,
}
impl Train_1_beebook_deterministic {
pub fn new() -> Train_1_beebook_deterministic {
//values: ''
let mut m: Train_1_beebook_deterministic = Default::default();
m.init();
return m;
}
fn init(&mut self) {
self.nxt = BRelation::new(vec![BTuple::from_refs(&ROUTES::R1, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::L, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::C)])), BTuple::from_refs(&ROUTES::R2, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::L, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::E), BTuple::from_refs(&BLOCKS::E, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::G)])), BTuple::from_refs(&ROUTES::R3, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::L, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::N)])), BTuple::from_refs(&ROUTES::R4, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::M, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::G)])), BTuple::from_refs(&ROUTES::R5, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::M, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::N)])), BTuple::from_refs(&ROUTES::R6, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::C, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::L)])), BTuple::from_refs(&ROUTES::R7, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::G, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::E), BTuple::from_refs(&BLOCKS::E, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::L)])), BTuple::from_refs(&ROUTES::R8, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::N, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::D), BTuple::from_refs(&BLOCKS::D, &BLOCKS::B), BTuple::from_refs(&BLOCKS::B, &BLOCKS::A), BTuple::from_refs(&BLOCKS::A, &BLOCKS::L)])), BTuple::from_refs(&ROUTES::R9, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::G, &BLOCKS::F), BTuple::from_refs(&BLOCKS::F, &BLOCKS::K), BTuple::from_refs(&BLOCKS::K, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::M)])), BTuple::from_refs(&ROUTES::R10, &BRelation::new(vec![BTuple::from_refs(&BLOCKS::N, &BLOCKS::J), BTuple::from_refs(&BLOCKS::J, &BLOCKS::I), BTuple::from_refs(&BLOCKS::I, &BLOCKS::H), BTuple::from_refs(&BLOCKS::H, &BLOCKS::M)]))]);
self.fst = BRelation::new(vec![BTuple::from_refs(&ROUTES::R1, &BLOCKS::L), BTuple::from_refs(&ROUTES::R2, &BLOCKS::L), BTuple::from_refs(&ROUTES::R3, &BLOCKS::L), BTuple::from_refs(&ROUTES::R4, &BLOCKS::M), BTuple::from_refs(&ROUTES::R5, &BLOCKS::M), BTuple::from_refs(&ROUTES::R6, &BLOCKS::C), BTuple::from_refs(&ROUTES::R7, &BLOCKS::G), BTuple::from_refs(&ROUTES::R8, &BLOCKS::N), BTuple::from_refs(&ROUTES::R9, &BLOCKS::G), BTuple::from_refs(&ROUTES::R10, &BLOCKS::N)]);
self.lst = BRelation::new(vec![BTuple::from_refs(&ROUTES::R1, &BLOCKS::C), BTuple::from_refs(&ROUTES::R2, &BLOCKS::G), BTuple::from_refs(&ROUTES::R3, &BLOCKS::N), BTuple::from_refs(&ROUTES::R4, &BLOCKS::G), BTuple::from_refs(&ROUTES::R5, &BLOCKS::N), BTuple::from_refs(&ROUTES::R6, &BLOCKS::L), BTuple::from_refs(&ROUTES::R7, &BLOCKS::L), BTuple::from_refs(&ROUTES::R8, &BLOCKS::L), BTuple::from_refs(&ROUTES::R9, &BLOCKS::M), BTuple::from_refs(&ROUTES::R10, &BLOCKS::M)]);
let mut _ic_set_0 = BRelation::<BLOCKS, ROUTES>::new(vec![]);
for _ic_b_1 in self._BLOCKS.clone().iter().cloned() {
for _ic_r_1 in self._ROUTES.clone().iter().cloned() {
if (self.nxt.domain().elementOf(&_ic_r_1).and(&self.nxt.functionCall(&_ic_r_1).domain().elementOf(&_ic_b_1).or(&self.nxt.functionCall(&_ic_r_1).range().elementOf(&_ic_b_1)))).booleanValue() {
_ic_set_0 = _ic_set_0._union(&BRelation::<BLOCKS, ROUTES>::new(vec![BTuple::from_refs(&_ic_b_1, &_ic_r_1)]));
}
}
}
self.rtbl = _ic_set_0;
self._BLOCKS = BSet::new(vec![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]);
self._ROUTES = BSet::new(vec![ROUTES::R1, ROUTES::R2, ROUTES::R3, ROUTES::R4, ROUTES::R5, ROUTES::R6, ROUTES::R7, ROUTES::R8, ROUTES::R9, ROUTES::R10]);
self.resrt = BSet::new(vec![]).clone().clone();
self.resbl = BSet::new(vec![]).clone().clone();
self.rsrtbl = BRelation::new(vec![]).clone().clone();
self.OCC = BSet::new(vec![]).clone().clone();
self.TRK = BRelation::new(vec![]).clone().clone();
self.frm = BSet::new(vec![]).clone().clone();
self.LBT = BSet::new(vec![]).clone().clone();
}
pub fn get_fst(&self) -> BRelation<ROUTES, BLOCKS> {
return self.fst.clone();
}
pub fn get_lst(&self) -> BRelation<ROUTES, BLOCKS> {
return self.lst.clone();
}
pub fn get_nxt(&self) -> BRelation<ROUTES, BRelation<BLOCKS, BLOCKS>> {
return self.nxt.clone();
}
pub fn get_rtbl(&self) -> BRelation<BLOCKS, ROUTES> {
return self.rtbl.clone();
}
pub fn get_LBT(&self) -> BSet<BLOCKS> {
return self.LBT.clone();
}
pub fn get_TRK(&self) -> BRelation<BLOCKS, BLOCKS> {
return self.TRK.clone();
}
pub fn get_frm(&self) -> BSet<ROUTES> {
return self.frm.clone();
}
pub fn get_OCC(&self) -> BSet<BLOCKS> {
return self.OCC.clone();
}
pub fn get_resbl(&self) -> BSet<BLOCKS> {
return self.resbl.clone();
}
pub fn get_resrt(&self) -> BSet<ROUTES> {
return self.resrt.clone();
}
pub fn get_rsrtbl(&self) -> BRelation<BLOCKS, ROUTES> {
return self.rsrtbl.clone();
}
pub fn get__BLOCKS(&self) -> BSet<BLOCKS> {
return self._BLOCKS.clone();
}
pub fn get__ROUTES(&self) -> BSet<ROUTES> {
return self._ROUTES.clone();
}
pub fn route_reservation(&mut self, mut r: ROUTES) -> () {
let mut _ld_resrt = self.resrt.clone();
let mut _ld_rsrtbl = self.rsrtbl.clone();
let mut _ld_resbl = self.resbl.clone();
self.resrt = _ld_resrt._union(&BSet::new(vec![r])).clone().clone();
self.rsrtbl = _ld_rsrtbl._union(&self.rtbl.rangeRestriction(&BSet::new(vec![r]))).clone().clone();
self.resbl = _ld_resbl._union(&self.rtbl.inverse().relationImage(&BSet::new(vec![r]))).clone().clone();
}
pub fn route_freeing(&mut self, mut r: ROUTES) -> () {
let mut _ld_frm = self.frm.clone();
let mut _ld_resrt = self.resrt.clone();
self.resrt = _ld_resrt.difference(&BSet::new(vec![r])).clone().clone();
self.frm = _ld_frm.difference(&BSet::new(vec![r])).clone().clone();
}
pub fn FRONT_MOVE_1(&mut self, mut r: ROUTES) -> () {
let mut _ld_OCC = self.OCC.clone();
let mut _ld_LBT = self.LBT.clone();
self.OCC = _ld_OCC._union(&BSet::new(vec![self.fst.functionCall(&r)])).clone().clone();
self.LBT = _ld_LBT._union(&BSet::new(vec![self.fst.functionCall(&r)])).clone().clone();
}
pub fn FRONT_MOVE_2(&mut self, mut b: BLOCKS) -> () {
self.OCC = self.OCC._union(&BSet::new(vec![self.TRK.functionCall(&b)])).clone().clone();
}
pub fn BACK_MOVE_1(&mut self, mut b: BLOCKS) -> () {
let mut _ld_rsrtbl = self.rsrtbl.clone();
let mut _ld_resbl = self.resbl.clone();
let mut _ld_OCC = self.OCC.clone();
let mut _ld_LBT = self.LBT.clone();
self.OCC = _ld_OCC.difference(&BSet::new(vec![b])).clone().clone();
self.rsrtbl = _ld_rsrtbl.domainSubstraction(&BSet::new(vec![b])).clone().clone();
self.resbl = _ld_resbl.difference(&BSet::new(vec![b])).clone().clone();
self.LBT = _ld_LBT.difference(&BSet::new(vec![b])).clone().clone();
}
pub fn BACK_MOVE_2(&mut self, mut b: BLOCKS) -> () {
let mut _ld_rsrtbl = self.rsrtbl.clone();
let mut _ld_resbl = self.resbl.clone();
let mut _ld_OCC = self.OCC.clone();
let mut _ld_LBT = self.LBT.clone();
self.OCC = _ld_OCC.difference(&BSet::new(vec![b])).clone().clone();
self.rsrtbl = _ld_rsrtbl.domainSubstraction(&BSet::new(vec![b])).clone().clone();
self.resbl = _ld_resbl.difference(&BSet::new(vec![b])).clone().clone();
self.LBT = _ld_LBT.difference(&BSet::new(vec![b]))._union(&BSet::new(vec![self.TRK.functionCall(&b)])).clone().clone();
}
pub fn point_positionning(&mut self, mut r: ROUTES) -> () {
self.TRK = self.TRK.domainSubstraction(&self.nxt.functionCall(&r).domain()).rangeSubstraction(&self.nxt.functionCall(&r).range())._union(&self.nxt.functionCall(&r)).clone().clone();
}
pub fn route_formation(&mut self, mut r: ROUTES) -> () {
self.frm = self.frm._union(&BSet::new(vec![r])).clone().clone();
}
}
#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
use btypes::binteger::BInteger;
use btypes::bboolean::BBoolean;
use btypes::bobject::BObject;
mod Train_1_beebook_deterministic;
#[derive(Default, Debug)]
pub struct Train_1_beebook_deterministic_exec {
counter: BInteger,
_Train_1_beebook_deterministic: Train_1_beebook_deterministic::Train_1_beebook_deterministic,
}
impl Train_1_beebook_deterministic_exec {
pub fn new() -> Train_1_beebook_deterministic_exec {
//values: ''
let mut m: Train_1_beebook_deterministic_exec = Default::default();
m.init();
return m;
}
fn init(&mut self) {
self.counter = BInteger::new(b"0");
self._Train_1_beebook_deterministic = Train_1_beebook_deterministic::Train_1_beebook_deterministic::new();
}
pub fn get_counter(&self) -> BInteger {
return self.counter.clone();
}
pub fn simulate(&mut self) -> () {
while (self.counter.less(&BInteger::new(b"10000"))).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::new(b"1"));
}
}
}
fn main() {
let mut exec = Train_1_beebook_deterministic_exec::new();
exec.simulate();
}
#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
use btypes::bboolean::BBoolean;
use btypes::bset::BSet;
use btypes::bobject::BObject;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub enum PID {
process1,
process2,
process3
}
impl PID {
pub fn equal(&self, other: &PID) -> BBoolean { BBoolean::new(*self == *other)}
pub fn unequal(&self, other: &PID) -> BBoolean { BBoolean::new(*self != *other)}
}
impl BObject for PID {}
impl Default for PID {
fn default() -> Self { PID::process1 }
}
impl fmt::Display for PID {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match *self {
PID::process1 => write!(f, "process1"),
PID::process2 => write!(f, "process2"),
PID::process3 => write!(f, "process3"),
}
}
}
#[derive(Default, Debug)]
pub struct scheduler_deterministic {
active: BSet<PID>,
_ready: BSet<PID>,
waiting: BSet<PID>,
_PID: BSet<PID>,
}
impl scheduler_deterministic {
pub fn new() -> scheduler_deterministic {
//values: ''
let mut m: scheduler_deterministic = Default::default();
m.init();
return m;
}
fn init(&mut self) {
self._PID = BSet::new(vec![PID::process1, PID::process2, PID::process3]);
self.active = BSet::new(vec![]).clone().clone();
self._ready = BSet::new(vec![]).clone().clone();
self.waiting = BSet::new(vec![]).clone().clone();
}
pub fn get_active(&self) -> BSet<PID> {
return self.active.clone();
}
pub fn get__ready(&self) -> BSet<PID> {
return self._ready.clone();
}
pub fn get_waiting(&self) -> BSet<PID> {
return self.waiting.clone();
}
pub fn get__PID(&self) -> BSet<PID> {
return self._PID.clone();
}
pub fn _new(&mut self, mut pp: PID) -> () {
if (self._PID.elementOf(&pp).and(&self.active.notElementOf(&pp)).and(&self._ready._union(&self.waiting).notElementOf(&pp))).booleanValue() {
self.waiting = self.waiting._union(&BSet::new(vec![pp])).clone().clone();
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
pub fn del(&mut self, mut pp: PID) -> () {
if (self.waiting.elementOf(&pp)).booleanValue() {
self.waiting = self.waiting.difference(&BSet::new(vec![pp])).clone().clone();
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
pub fn ready(&mut self, mut rr: PID) -> () {
if (self.waiting.elementOf(&rr)).booleanValue() {
self.waiting = self.waiting.difference(&BSet::new(vec![rr])).clone().clone();
if (self.active.equal(&BSet::new(vec![]))).booleanValue() {
self.active = BSet::new(vec![rr]).clone().clone();
} else {
self._ready = self._ready._union(&BSet::new(vec![rr])).clone().clone();
}
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
pub fn swap(&mut self, mut pp: PID) -> () {
if (self.active.unequal(&BSet::new(vec![]))).booleanValue() {
self.waiting = self.waiting._union(&self.active).clone().clone();
if (self._ready.equal(&BSet::new(vec![]))).booleanValue() {
self.active = BSet::new(vec![]).clone().clone();
} else {
self.active = BSet::new(vec![pp]).clone().clone();
self._ready = self._ready.difference(&BSet::new(vec![pp])).clone().clone();
}
} else {
panic!("ERROR: called SELECT-function with incompatible parameters!");
}
}
}
#![ allow( dead_code, unused_imports, unused_mut, non_snake_case, non_camel_case_types, unused_assignments ) ]
use std::fmt;
use rand::{thread_rng, Rng};
use btypes::butils;
use btypes::binteger::BInteger;
use btypes::bboolean::BBoolean;
use btypes::bobject::BObject;
mod scheduler_deterministic;
#[derive(Default, Debug)]
pub struct scheduler_deterministic_exec {
counter: BInteger,
_scheduler_deterministic: scheduler_deterministic::scheduler_deterministic,
}
impl scheduler_deterministic_exec {
pub fn new() -> scheduler_deterministic_exec {
//values: ''
let mut m: scheduler_deterministic_exec = Default::default();
m.init();
return m;
}
fn init(&mut self) {
self.counter = BInteger::new(b"0");
self._scheduler_deterministic = scheduler_deterministic::scheduler_deterministic::new();
}
pub fn get_counter(&self) -> BInteger {
return self.counter.clone();
}
pub fn simulate(&mut self) -> () {
while (self.counter.less(&BInteger::new(b"300000"))).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::new(b"1"));
}
}
}
fn main() {
let mut exec = scheduler_deterministic_exec::new();
exec.simulate();
}
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment