FORCE (First-Order synthesiser via oRthogonal sliCEs)

This repository contains the implementation of FORCE, a tool for synthesizing first-order formulas from a set of FO structures (as examples); with the integration in DuoAI. The research paper for FORCE is "Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference", to appear in ICLP 2025.

Dependencies

• Clingo (>= 5.5.0)
• CMake (for FORCE)
• Make (for DuoAI)

Building

To build FORCE, you might need to adjust the C++ compiler and libclingo locations in the src-c/CMakeLists.txt file.

cd src-c/
cmake -H. -Bbuild -DCMAKE_BUILD_TYPE=Release
cmake --build build

To build DuoAI, you need first replace #include "Solver2.h" in main.cpp and InvRefiner.h into #include "Solver.h"

cd src-c/
make

Usage

Given a distributed protocol, PROTOCOL_NAME (=paxos,..), there are 6 settings to synthesise the invariant corresponding to the experiments in the paper.:

time ./main PROTOCOL_NAME --parallel_instance=top_down_or_bottom_up
time ./main PROTOCOL_NAME --parallel_instance=top_down_or_bottom_up --cutoff=0
time ./main PROTOCOL_NAME --parallel_instance=top_down_or_bottom_up --fix=1
time ./main PROTOCOL_NAME --parallel_instance=top_down_or_bottom_up --fix=1 --cutoff=0
time ./build/main PROTOCOL_NAME --parallel_instance=top_down_or_bottom_up --cutoff=1
time ./build/main PROTOCOL_NAME --parallel_instance=top_down_or_bottom_up --cutoff=0

The first command runs the original DuoAI's invariant enumeration (with two unsound pruning); then --cutoff=0 and --fix=1 are parameters fixing the unsound pruning in DuoAI. The last two commands run FORCE with and without the prefix cutoff.

Structure

• protocols/: The distributed protocols (mostly) from DuoAI's benchmark.

• traces/: The protocol traces generated by the original DuoAI's simulation.

• config/: The configuration files for the invariant synthesis.

The config and traces generation need extra setups for DuoAI, so we simply provide the generated files in this repository (as they are inputs of the synthesis).

• components_asp/: The ASP encoding of the invariant synthesis.

• src-c/: The C++ implementation of original DuoAI and FORCE (in Solver2 files).