./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>"
./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
# JavaScript/TypeScript
./gradlew run -Planguage="ts"[-Pbig_integer="true/false"-Pminint="minint"-Pmaxint="maxint"-Pdeferred_set_size="size"-PuseConstraintSolving="true/false"-PforModelchecking="true/false"]-Pfile="<path_relative_to_project_directory>"
./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
# 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>"
./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>"
...
@@ -441,6 +441,10 @@ Remarks:
...
@@ -441,6 +441,10 @@ Remarks:
# Rust
# 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>"
./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:
Default Values:
big_integer: false
big_integer: false
minint: -2147483648
minint: -2147483648
...
@@ -448,6 +452,7 @@ maxint: 2147483647
...
@@ -448,6 +452,7 @@ maxint: 2147483647
deferred_set_size: 10
deferred_set_size: 10
useConstraintSolving: false
useConstraintSolving: false
forModelchecking: false
forModelchecking: false
```
```
`-PuseConstraintSolving` is in an experimental stage.
`-PuseConstraintSolving` is in an experimental stage.
...
@@ -594,6 +599,15 @@ The right-hand side shows the State View consisting of the variables', constants
...
@@ -594,6 +599,15 @@ The right-hand side shows the State View consisting of the variables', constants
7. Open Interactive Validation Document for TrafficLight (`TrafficLight.html`)
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)
## Steps from B Model to Execution of the Generated Code (with primitive types)