FalCAuN-ARCH-COMP

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.

Requirements

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.

• MATLAB with Simulink and Stateflow. Some benchmarks require additional toolboxes.
• kscript

Usage

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.

On the benchmarks

FalCAuN can handle the following benchmarks

• AT
  • AT1
  • AT2
  • AT6{a,b,c}
    • For AT6{a,b}, although FalCAuN can handle "input Case 1", FalCAuN cannot handle "input Case 2" because the control points of the input and the observation point of the outputs must be the same.
• CC
  • CC1
  • CC2
  • CC3
  • (The input signals generated by FalCAuN are with control points for each 10 second, which is more strict than "input Case 2")
• SC
  • Although FalCAuN can handle "input Case 1", FalCAuN cannot handle "input Case 2" because the control points of the input and the observation point of the outputs must be the same.
• pacemaker
  • pacemaker

Note on the unsupported benchmarks

AFC (powertrain)

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.

AT (transmission)

FalCAuN can falsify AT1, AT2, and AT6{a,b,c}. 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).

NN (neural)

Encoding of always_[1.0, 37.0] makes the LTL formula too large (same as AFC).

WT

• WT1, WT2, WT3, WT4

CC (Chasing Cars)

FalCAuN can falsify CC1, CC2, and CC3. However, CC4 and CC5 are infeasible because the STL formulas are encoded to huge LTL formulas (same reason as AFC).

F16 (f16-gcas)

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.

sabo

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.

How to deploy

We can deploy the scripts in this repository to the directory of ARCH-COMP. We assume that the repository of ARCH-COMP exists at ../Codes/ARCH-COMP.

The usage is as follows.

make -C utils/ -f Makefile.deploy