diff --git a/README.md b/README.md index 0bfbe2c404599777b2ee2416155fcd6fbb83f5e2..146bb88c93642af615210acec57038f43d91f1d9 100644 --- a/README.md +++ b/README.md @@ -433,7 +433,7 @@ Remarks: ./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"] -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 ./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: # 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 @@ -448,6 +452,7 @@ maxint: 2147483647 deferred_set_size: 10 useConstraintSolving: false forModelchecking: false + ``` `-PuseConstraintSolving` is in an experimental stage. @@ -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`) +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