This repository contains the materials to execute FalCAuN with the benchmark for ARCH-COMP's falsification track.
To execute the scripts in this repository. You need to install FalCAuN.
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.
For archival purposes, we keep the old shell scripts used until ARCH-COMP 2023. The usage is similar to the current scripts, for example, cd ./AT && ./run_falcaun_AT1.sh.
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).
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.
"Instance 1" is not available for SB benchmarks. FalCAuN does not support piecewise constant inputs.