Examples
The following is a list of examples. To run the Kotlin examples, you need to install kscript. To run the Jupyter example, you need to set up Jupyter with the kotlin-jupyter kernel. Some examples use the Python binding and require JEP.
Examples not requiring MATLAB/Simulink
The following examples do not require MATLAB/Simulink.
| Name | Description | Links |
|---|---|---|
| Mealy | A small Mealy machine | Kotlin Jupyter |
| Button Detector | A buggy button detector modeled as a Mealy machine | Kotlin |
| Bouncing Ball | The bouncing ball benchmark checked against an STL formula | Kotlin |
| Counter | A toy system with a counter | Jupyter |
| Python SUL | A Mealy machine implemented in Python | Python |
Examples requiring MATLAB/Simulink
The following examples require MATLAB/Simulink.
| Name | Description | Links |
|---|---|---|
| AT1 | The automatic transmission benchmark against the S1 formula in ARCH-COMP | Kotlin |
| AT2 | The automatic transmission benchmark against the S2 formula in ARCH-COMP | Kotlin |
| AT6a | The automatic transmission benchmark against the S6a formula in ARCH-COMP | Kotlin |
| AT6b | The automatic transmission benchmark against the S6b formula in ARCH-COMP | Kotlin |
| AT6c | The automatic transmission benchmark against the S6c formula in ARCH-COMP | Kotlin |
| AT6abc | The automatic transmission benchmark against the S6abc formula in ARCH-COMP | Kotlin |
| CC1 | The chasing cars benchmark against the CC1 formula in ARCH-COMP | Kotlin |
| CC2 | The chasing cars benchmark against the CC2 formula in ARCH-COMP | Kotlin |
| CC3 | The chasing cars benchmark against the CC3 formula in ARCH-COMP | Kotlin |
| CC4 | The chasing cars benchmark against the CC4 formula in ARCH-COMP | Kotlin |
| CCx | The chasing cars benchmark against the CCx formula in ARCH-COMP | Kotlin |