This repository contains the materials to execute FalCAuN with the benchmark for ARCH-COMP's falsification track.
Note: the script in this repository requires the development version of FalCAuN (as of 2024-04-25), where we target scripting via Kotlin in addition to the original command line interface.
To execute the scripts in this repository. You need to install FalCAuN. As of 2024-04-25, the raw_simulink_model branch is required.
In addition to FalCAuN, you need to install the following tools.
You can run the experiment by running the scripts, for example, cd AT && ./AT1.main.kts. Since the scripts are sensitive to the current directory, you need to run the scripts in the directory of the benchmark. You can also specify the number of repetitions, for example, cd AT && ./AT1.main.kts 10.
FalCAuN can handle the following benchmarks
ATAT1AT2AT6{a,b,c,abc}
CCCC1CC2CC3CC4
SCPM
FalCAuN can execute the AFC model but for any requirements, it crashes due to stack overflow. This is because, in FalCAuN, always_[11, 50] is encoded to an LTL formulas with 50 nests of next operators, which is too large for its back-end model checker.
FalCAuN can falsify AT1, AT2, and AT6{a,b,c,abc}. However, AT5{1,2,3,4} are infeasible because encoding of ev_[0.001, 0.1] is impossible or makes the LTL formula super huge (same as AFC).
Encoding of always_[1.0, 37.0] makes the LTL formula too large (same as AFC).
- WT1, WT2, WT3, WT4
FalCAuN can falsify CC1, CC2, CC3, and CC4. However, CC5 and CCx are infeasible because the STL formulas are encoded to huge LTL formulas (same reason as AFC).
FalCAuN cannot handle F16 benchmark because it is not a pure Simulink model but requires quite a lot of wrapper in MATLAB, which is currently not supported.
FalCAuN cannot handle sabo benchmark because it is not a Simulink model but a model implemented in python. It is a future work to support such models.