Skip to content

Commit a37343a

Browse files
committed
Update README
1 parent 09deee9 commit a37343a

File tree

1 file changed

+15
-1
lines changed

1 file changed

+15
-1
lines changed

README.md

+15-1
Original file line numberDiff line numberDiff line change
@@ -433,21 +433,26 @@ Remarks:
433433
./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>"
434434

435435
# JavaScript/TypeScript
436-
./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>"
436+
./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>"
437437

438438
# C
439439
./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>"
440440

441441
# Rust
442442
./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>"
443443

444+
445+
446+
serverLink: Server Link is the link to your website if you want to generate interactive validation HTML documents
447+
444448
Default Values:
445449
big_integer: false
446450
minint: -2147483648
447451
maxint: 2147483647
448452
deferred_set_size: 10
449453
useConstraintSolving: false
450454
forModelchecking: false
455+
451456
```
452457
453458
`-PuseConstraintSolving` is in an experimental stage.
@@ -594,6 +599,15 @@ The right-hand side shows the State View consisting of the variables', constants
594599
7. Open Interactive Validation Document for TrafficLight (`TrafficLight.html`)
595600
596601
602+
In case you want to link the generated files to a website, then your step 3 is as follows:
603+
604+
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.,
605+
`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
606+
607+
Furthermore, there is another step between step 6 and 7:
608+
- Execute the `.js`-File to link your JavaScript files with your website: `node <compatibility>-compatibility.js``` i.e., `node TrafficLight-compatibility.js`
609+
610+
597611
## Steps from B Model to Execution of the Generated Code (with primitive types)
598612
599613
### Example 1: Lift

0 commit comments

Comments
 (0)