B2Program

This is the code generator B2Program for generating code from B to other programming languages (Java, C++, JavaScript/TypeScript). Currently, code generation for Prolog and Rust are in progress. The work for Python, Clojure and C has begun but not continued.

Paper: https://www.researchgate.net/publication/337441241_A_Multi-target_Code_Generator_for_High-Level_B

Citations:

• B2Program Paper:

@InProceedings{b2program,
author = {Vu, Fabian and Hansen, Dominik and K{\"{o}}rner, Philipp and Leuschel, Michael},
year = {2019},
month = {11},
pages = {456-473},
Booktitle = {Proceedings {iFM} 2019},
title = {A Multi-target Code Generator for High-Level B},
isbn = {978-3-030-34967-7},
doi = {10.1007/978-3-030-34968-4_25}
}

• B2Program Validation Documents Paper:

@InProceedings{b2program_js,
author="Vu, Fabian
and Happe, Christopher
and Leuschel, Michael",
editor="Groote, Jan Friso
and Huisman, Marieke",
title="Generating Domain-Specific Interactive Validation Documents",
booktitle="Formal Methods for Industrial Critical Systems",
year="2022",
publisher="Springer International Publishing",
address="Cham",
pages="32--49",
isbn="978-3-031-15008-1"
}

• B2Program Validation Documents Journal Paper:

@article{b2program_js_journal,
	abstract = {Especially in industrial applications of formal modeling, validation is as important as verification. Thus, it is important to integrate the stakeholders'and the domain experts'feedback as early as possible. In this work, we propose two approaches to enable this: (1) a static export of an animation trace into a single HTML file, and (2) a dynamic export of a classical B model as an interactive HTML document, both based on domain-specific visualizations. For the second approach, we extend the high-level code generator B2Program by JavaScript and integrate VisB visualizations alongside SimB simulations with timing, probabilistic and interactive elements. An important aspect of this work is to ease communication between modelers and domain experts. This is achieved by implementing features to run simulations, sharing animated traces with descriptions and giving feedback to each other. This work also evaluates the performance of the generated JavaScript code compared with existing approaches with Java and C++ code generation as well as the animator, constraint solver, and model checker ProB.},
	author = {Vu, Fabian and Happe, Christopher and Leuschel, Michael},
	da = {2024/04/01},
	date-added = {2024-04-15 22:43:55 +0200},
	date-modified = {2024-04-15 22:43:55 +0200},
	doi = {10.1007/s10009-024-00739-0},
	id = {Vu2024},
	isbn = {1433-2787},
	journal = {International Journal on Software Tools for Technology Transfer},
	number = {2},
	pages = {147--168},
	title = {Generating interactive documents for domain-specific validation of formal models},
	ty = {JOUR},
	url = {https://doi.org/10.1007/s10009-024-00739-0},
	volume = {26},
	year = {2024},
	Bdsk-Url-1 = {https://doi.org/10.1007/s10009-024-00739-0}}

• B2Program Model Checking Code Generation Paper:

@InProceedings{b2program_mc,
author="Vu, Fabian
and Brandt, Dominik
and Leuschel, Michael",
editor="Riesco, Adrian
and Zhang, Min",
title="Model Checking B Models via High-Level Code Generation",
booktitle="Formal Methods  and Software Engineering",
year="2022",
publisher="Springer International Publishing",
address="Cham",
pages="334--351",
isbn="978-3-031-17244-1"
}

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, C++ and Rust)
• Code generation of interactive domain-specific visualizations (from VisB) in HTML and JavaScript/TypeScript

Note:

• The implementation of the B types in C++ uses persistent set from: https://github.com/arximboldi/immer
• The library must first be installed before the generated C++ code can be used.
• The generated code for C works for a subset of the generated code that works for Java and C++.
• Sets and couples are not supported for C. Including other machines is not supported in C, too. The only types that are implemented for C are BInteger and BBoolean. An example where code generation for C works is the machine Lift.
• Executing all tests requires building Java B Types and installing C++ B Types

Interactive Validation Document

TrafficLight

Pitman Controller

Landing Gear Hydraulic Circuit

Landing Gear Gears and Doors

Performance

Performance Evaluation for Execution described in benchmarks/execution/README.md.

Performance Evaluation for Model Checking described in benchmarks/model_checking/README.md.

Build Java B Types

Primitive Integer: make btypes_primitives

Big Integer: make btypes_big_integer

Install C++ B Types

mkdir build && cd build
cmake ..
make install

Make sure that the immer library and gmpxx library (for big integers) are installed before.

Supported Subset of B

Machine sections:

Note that code is not generated from INVARIANT and ASSERTIONS. These constructs are used for verifying the machine only. CONSTRAINTS and DEFINITIONS clause are not supported for code generation.

Machine inclusion:

Other machine inclusion clauses (SEES, USES, PROMOTES and REFINES) are not supported yet.

Logical Predicates:

Restriction: As universal quantifications and existential quantifications are quantified constructs, the predicate P must constraint the value of the variables x1, ..., xn. P is a conjunction of n conjuncts where the i-th conjunct must constraint xi for each i in {1,...,n}.

Equality:

Booleans:

Sets:

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}.

Numbers:

Restrictions:

INTEGER, NATURAL and NATURAL1 are infinite sets. They are only supported on the right-hand side of a set predicate.

Set product and set summation 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}.

Relations:

Restriction: Set of Relation mostly grows up very fast. They are only supported on the right-hand side of a set predicate.

Functions:

Restriction: Lambda expressions 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}.

Sequences:

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.

Records:

Nested record accesses are also supported.

Strings:

Restriction: STRING is a infinite set. It is only supported on the right-hand side of a set predicate.

LET and IF-THEN-ELSE Expression and Predicate:

Substitution:

Functional Override and Record Access with assignment can be nested.

Preconditions and Assertions are constructs that are relevant for verification. They are ignored at code generation.

Assignments, Operation Calls, Choice from Set and Choice By Predicate can contain many variables on the left-hand side. Furthermore Choice By Predicate can use previous values of variables.

Restriction: Choice by Predicates 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}.

Comments are ignored during code generation. Furthermore trees and pragmas are not supported by B2Program.

Remarks:

• SELECT with ELSE Branches are not supported yet
• Non-determinism for model checking is only supported for top-level SELECT and PRE

Usage

Starting the code generator

Gradle

# Java
./gradlew run -Planguage="java" [-Pbig_integer="true/false" -Pminint="minint" -Pmaxint="maxint" -Pdeferred_set_size="size" -PuseConstraintSolving="true/false" -PforModelchecking="true/false"] -Pfile="<path_relative_to_project_directory>"

# C++
./gradlew run -Planguage="cpp" [-Pbig_integer="true/false" -Pminint="minint" -Pmaxint="maxint" -Pdeferred_set_size="size" -PuseConstraintSolving="true/false" -PforModelchecking="true/false"] -Pfile="<path_relative_to_project_directory>"

# Python
./gradlew run -Planguage="python" [-Pbig_integer="true/false" -Pminint="minint" -Pmaxint="maxint" -Pdeferred_set_size="size" -PuseConstraintSolving="true/false" -PforModelchecking="true/false"] -Pfile="<path_relative_to_project_directory>"

# JavaScript/TypeScript
./gradlew run -Planguage="ts" [-Pbig_integer="true/false" -Pminint="minint" -Pmaxint="maxint" -Pdeferred_set_size="size" -PuseConstraintSolving="true/false" -PforModelchecking="true/false" -Pserverlink="<serverLink>"] -Pfile="<path_relative_to_project_directory>"

# 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>"



serverLink: Server Link is the link to your website if you want to generate interactive validation HTML documents

Default Values:
big_integer: false
minint: -2147483648
maxint: 2147483647
deferred_set_size: 10
useConstraintSolving: false
forModelchecking: false

-PuseConstraintSolving is in an experimental stage.

JAR-File

1. Run ./gradlew fatJar to build the JAR-file
2. Generate code from the machine

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

Compile generated Code

Java

1. Build JAR for Java B Types (make btypes_primitives or make btypes_big_integer)
2. Move btypes_persistent.jar to same directory as the generated classes
3. javac -cp btypes_primitives-all.jar <files....>
4. Example: javac -cp btypes_primitives-all.jar TrafficLightExec.java TrafficLight.java (Code generated from TrafficLightExec.mch which includes TrafficLight.mch)

C++

1. Install C++ B Types or move them (see btypes_primitives or btypes_big_integer directory) to same directory as the generated classes
2. g++ -std=c++14 -O2 -march=native -g -DIMMER_NO_THREAD_SAFETY -o <executable> <main class>
3. Example: g++ -std=c++14 -O2 -flto -march=native -g -DIMMER_NO_THREAD_SAFETY -o TrafficLightExec.exec TrafficLightExec.cpp (TrafficLightExec.mch includes TrafficLight.mch, this command automatically compiles TrafficLight.cpp)

JavaScript/TypeScript

1. Move B types to same folder (see btypes_primitives or btypes_big_integer directory) as generated code
2. Move immutable library to same folder as generated code
3. tsc --target ES6 --moduleResolution node <files...>
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) 2. rename the file of the main-machine to main.rs
2. run cargo build --release

Execute generated code (manual simulation)

Java

1. Write a main function in the generated main class
2. java -cp :btypes_primitives-all.jar <main file>
3. Example: java -cp :btypes_primitives-all.jar TrafficLightExec

C++

1. Write a main function in the generated main class
2. ./<main file>
3. Example: ./TrafficLightExec.exec

JavaScript/TypeScript

1. Write a main function in the generated main class
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

Java

1. java -cp :btypes_primitives-all.jar <main file> <strategy> <threads> <caching>
2. Example: java -cp :btypes_primitives-all.jar TrafficLight mixed 6 true

C++

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}
• threads : NATURAL
• caching : {TRUE, FALSE}

Currently, there is also a Makefile which automizes these steps. Therefore, the B model must be in the top-level directory of this project, and execute these steps:

make b2program
make btypes_primitives (or make btypes_big_integer)
make <file> LANGUAGE=<language>

Example:

make b2program
make btypes_primitives
make CAN_BUS_tlc LANGUAGE=java

Execute generated interactive validation document

By specifying a visualization, B2Program also supports generating an interactive (HTML) validation document, i.e., an interactive domain-specific visualization from VisB. Here, the specified language must be JavaScript/TypeScript. An example of such an interactive validation document is shown below.

The interactive domain-specific validation document consists of the VisB View, the Operations View, the History View, the Scenario View, and the State View. The VisB View contains the domain-specific visualization as an SVG image. Here, it is possible for a domain expert to execute events (by clicking on the graphical elements), and to inspect the model's state. The Operations View shows operations that are enabled in the model's current state. It makes it possible for a domain expert to animate the model. Furthermore, it shows enabled events, and parameters for which an event is enabled. Within the history view, a domain expert can inspect the currently animated trace, or run the trace with delay (10ms and 500ms). Here, it is also possible to step within the trace, and to import/export the trace, targeting other validation documents or ProB2-UI. Imported trace will be shown in the Scenario View. The right-hand side shows the State View consisting of the variables', constants', sets', and invariants' values in mathematical B notation.

Steps to Interactive Validation Document (Example: Traffic Light)

1. Run ./gradlew fatJar to build the JAR-file
2. Move the built JAR-file B2Program-all-0.1.0-SNAPSHOT to the same folder as TrafficLight.mch and VisB files (TrafficLight.json as VisB Glue File, and TrafficLight.svg as SVG image)
3. Generate code for TrafficLight.mch and TrafficLight.json java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l ts -f TrafficLight.mch -v TrafficLight.json
4. Move B types to same folder (see btypes_primitives or btypes_big_integer directory) as generated code
5. Move immutable library to same folder as generated code
6. Compile generated TypeScript files tsc --target ES6 --moduleResolution node TrafficLight.ts
7. Open Interactive Validation Document for TrafficLight (TrafficLight.html)

In case you want to link the generated files to a website, then your step 3 is as follows:

3. Generate code for TrafficLight.mch and TrafficLight.json java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l ts -f TrafficLight.mch -v TrafficLight.json -sl <link>, i.e., TrafficLight.mch and TrafficLight.json java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l ts -f TrafficLight.mch -v TrafficLight.json -sl https://favu100.github.io/b2program/visualizations/TrafficLight for this repository

Furthermore, there is another step between step 6 and 7:

• Execute the .js-File to link your JavaScript files with your website: node <compatibility>-compatibility.js i.e., node TrafficLight-compatibility.js

Steps from B Model to Execution of the Generated Code (with primitive types)

Example 1: Lift

The file for Lift.mch is in https://github.com/favu100/b2program/tree/master/src/test/resources/de/hhu/stups/codegenerator. Lift consists of operation to lift up and lift down and getting the floor.

Execution with manual simulation

Java

• 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 java -f Lift.mch
• Write a main method in Lift.java

public static void main(String[] args) {
    Lift lift = new Lift();
    lift.inc();
    lift.inc();
    lift.inc();
    System.out.println(lift.getFloor());
}

• Build B types in btypes_primitives ./gradlew fatJar in the belonging directory or execute make which builds btypes_primitives and move it to this folder
• Move btypes_primitives-all.jar to the same directory as Lift.java
• Compile Lift.java with javac -cp btypes_primitives-all.jar Lift.java
• Execute the compiled file for Lift.java with java -cp :btypes_primitives-all.jar Lift
• Output: 3

C++

• 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 java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l -cpp -f Lift.mch
• Write a main method in Lift.cpp

int main() {
    Lift lift;
    lift.inc();
    lift.inc();
    lift.inc();
    cout << lift.getFloor() << "\n";;
    return 0;
}

• Install C++ B types with

mkdir build & cd build
cmake ..
make install

• Compile Lift.cpp with g++ -std=c++14 -O2 -flto -march=native -g -DIMMER_NO_THREAD_SAFETY -o Lift.exec Lift.cpp
• Execute Lift.exec with ./Lift

JavaScript/TypeScript

• 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 ts -f Lift.mch
• Write additional code executing generated functions in Lift.ts

let lift: Lift = new Lift();
lift.inc();
lift.inc();
lift.inc();
console.log(lift.getFloor().toString());

• Move btypes_primitives for js to the same directory as Lift.ts
• Transpile Lift.ts to Lift.js with tsc --target ES6 --moduleResolution node Lift.ts
• 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
• Write additional code executing generated functions of the Lift-machine

  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

• 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 java -f Lift.mch -mc true
• Build B types in btypes_primitives ./gradlew fatJar in the belonging folder or execute makewhich builds btypes_primitives and move it to this folder
• Move btypes_primitives-all.jar to the same folder as Lift.java
• Compile Lift.java with javac -cp btypes_primitives-all.jar Lift.java
• Execute the compiled file for Lift.java with java -cp :btypes_primitives-all.jar Lift mixed 1 false

C++

• 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 java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l cpp -f Lift.mch -mc true
• Install C++ B types with

mkdir build & cd build
cmake ..
make install

• Compile Lift.cpp with g++ -std=c++14 -O2 -flto -march=native -g -DIMMER_NO_THREAD_SAFETY -o Lift.exec Lift.cpp
• 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
• 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. Cruise_finite1_deterministic_exec contains an operation for executing a cycle in the state space of Cruise_finite1_deterministic 100.000 times. Furthermore it has getter operations for all variables.

Execution with manual simulation

Java

• 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 java -f Cruise_finite1_deterministic.mch
• Write a main method in Cruise_finite1_deterministic_exec.java

public static void main(String[] args) {
    Cruise_finite1_deterministic_exec cruise = new Cruise_finite1_deterministic_exec();
    cruise.simulate();
    System.out.println(cruise.getCruiseAllowed());
    System.out.println(cruise.getCruiseActive());
    System.out.println(cruise.getVehicleAtCruiseSpeed());
    System.out.println(cruise.getVehicleCanKeepSpeed());
    System.out.println(cruise.getVehicleTryKeepSpeed());
    System.out.println(cruise.getSpeedAboveMax());
    System.out.println(cruise.getVehicleTryKeepTimeGap());
    System.out.println(cruise.getCruiseSpeedAtMax());
    System.out.println(cruise.getObstaclePresent());
    System.out.println(cruise.getObstacleDistance());
    System.out.println(cruise.getObstacleRelativeSpeed());
    System.out.println(cruise.getObstacleStatusJustChanged());
    System.out.println(cruise.getCCInitialisationInProgress());
    System.out.println(cruise.getCruiseSpeedChangeInProgress());
}

• Build B types in btypes_primitives with ./gradlew fatJar in the belonging folder or execute makewhich builds btypes_primtives and move it to this folder
• Move btypes_primitives-all.jar to the same folder as the generated classes
• Compile Cruise_finite1_deterministic_exec.java and Cruise_finite1_deterministic.java with javac -cp btypes_primitives-all.jar Cruise_finite1_deterministic_exec.java Cruise_finite1_deterministic.java
• Execute the compiled file for Cruise_finite1_deterministic_exec.java with java -cp :btypes_primitives-all.jar Cruise_finite1_deterministic_exec
• Output:

false
false
false
false
false
false
false
false
false
ODnone
RSnone`
false
false
false

C++

• 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 cpp -f Cruise_finite1_deterministic_exec.mch
• Write a main method in Cruise_finite1_deterministic_exec.cpp

int main() {
    Cruise_finite1_deterministic_exec cruise;
    cruise.simulate();
    cout << cruise.getCruiseAllowed() << "\n";
    cout << cruise.getCruiseActive() << "\n";
    cout << cruise.getVehicleAtCruiseSpeed() << "\n";
    cout << cruise.getVehicleCanKeepSpeed() << "\n";
    cout << cruise.getVehicleTryKeepSpeed() << "\n";
    cout << cruise.getSpeedAboveMax() << "\n";
    cout << cruise.getVehicleTryKeepTimeGap() << "\n";
    cout << cruise.getCruiseSpeedAtMax() << "\n";
    cout << cruise.getObstaclePresent() << "\n";
    cout << cruise.getObstacleDistance() << "\n";
    cout << cruise.getObstacleRelativeSpeed() << "\n";
    cout << cruise.getObstacleStatusJustChanged() << "\n";
    cout << cruise.getCCInitialisationInProgress() << "\n";
    cout << cruise.getCruiseSpeedChangeInProgress() << "\n";
    return 0;
}

• Install C++ B types with

mkdir build & cd build
cmake ..
make install

• Compile Cruise_finite1_deterministic_exec.cpp with g++ -std=c++14 -O2 -flto -march=native -g -DIMMER_NO_THREAD_SAFETY -o Cruise_finite1_deterministic_exec.exec Cruise_finite1_deterministic_exec.cpp
• Execute Cruise_finite1_deterministic_exec.exec with ./Cruise_finite1_deterministic_exec.exec
• Output:

false
false
false
false
false
false
false
false
false
ODnone
RSnone`
false
false
false

JavaScript/TypeScript

• Run ./gradlew fatJar to build the JAR-file
• Move the built JAR-file B2Program-all-0.1.0-SNAPSHOT to the same directory as Cruise_finite1_deterministic_exec.mch
• Generate code for Cruise_finite1_deterministic_exec.mch with java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l ts -f Cruise_finite1_deterministic_exec.mch
• Write additional code executing generated functions in Cruise_finite1_deterministic_exec.ts

let cruise: Cruise_finite1_deterministic_exec = new Cruise_finite1_deterministic_exec();
cruise.simulate();
console.log(cruise.getCruiseAllowed().toString());
console.log(cruise.getCruiseActive().toString());
console.log(cruise.getVehicleAtCruiseSpeed().toString());
console.log(cruise.getVehicleCanKeepSpeed().toString());
console.log(cruise.getVehicleTryKeepSpeed().toString());
console.log(cruise.getSpeedAboveMax().toString());
console.log(cruise.getVehicleTryKeepTimeGap().toString());
console.log(cruise.getCruiseSpeedAtMax().toString());
console.log(cruise.getObstaclePresent().toString());
console.log(cruise.getObstacleDistance().toString());
console.log(cruise.getObstacleRelativeSpeed().toString());
console.log(cruise.getObstacleStatusJustChanged().toString());
console.log(cruise.getCCInitialisationInProgress().toString());
console.log(cruise.getCruiseSpeedChangeInProgress().toString());

• Move btypes_primitives for js to the same directory as Cruise_finite1_deterministic_exec.ts
• Transpile Cruise_finite1_deterministic_exec.ts and Cruise_finite1_deterministic.ts to Cruise_finite1_deterministic_exec.js and Cruise_finite1_deterministic.js with tsc --target ES6 --moduleResolution node Cruise_finite1_deterministic_exec.ts Cruise_finite1_deterministic.ts
• Execute the transpiled file with node --experimental-specifier-resolution=node Cruise_finite1_deterministic_exec.js
• Output:

false
false
false
false
false
false
false
false
false
ODnone
RSnone`
false
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
• Write additional code in main.rs

  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:

  false
  false
  false
  false
  false
  false
  false
  false
  false
  ODnone
  RSnone
  false
  false
  false

Model Checking

Java

• 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 java -f Cruise_finite1_deterministic.mch -mc true
• Build B types in btypes_primitives with ./gradlew fatJar in the belonging folder or execute makewhich builds btypes_primtives and move it to this folder
• Move btypes_primitives-all.jar to the same folder as the generated classes
• Compile Cruise_finite1_deterministic.java with javac -cp btypes_primitives-all.jar Cruise_finite1_deterministic.java
• Execute the compiled file for Cruise_finite1_deterministic.java with java -cp :btypes_primitives-all.jar Cruise_finite1_deterministic mixed 6 true

C++

• 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 cpp -f Cruise_finite1_deterministic.mch -mc true
• Install C++ B types with

mkdir build & cd build
cmake ..
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
• from the bmachine-directory, run cargo run --release -- mixed 6 true