CIF3Connector

CIF3Connector is a tool that enables redundant orchestration synthesis by bridging the Contract Automata Library (CATLib) and the Eclipse Supervisory Control Engineering Toolkit (ESCET). It translates contract automata models into the CIF3 input language, allowing users to cross-validate orchestration results between CATLib’s native synthesis and CIF3’s most permissive controller synthesis.

Features

• Translation: Converts .data files (CATLib format) into .cif files.
• Transition Encoding: Automatically encodes semi-controllable (lazy necessary) transitions into pairs of controllable and uncontrollable transitions, making them compatible with standard supervisory control theory.
• Redundant Synthesis: Supports a workflow for comparing synthesis results from two independent tools to increase confidence in verification outcomes.

Prerequisites

• Java Runtime Environment (JRE) v17: Required to run the JAR file.
• Eclipse ESCET (CIF3) v10 Required if you intend to perform synthesis and equivalence checking using the translated files.

Usage

The tool is provided as a JAR package and can be executed from the command line.

Basic Command Syntax

java -jar CIF3Connector.jar -i <input1.data> [<input2.data> ...] [-o <composition.cif> <orchestration.cif>] [-a]

Parameters

• -i: A required list of input contract automata files in .data format.
• -o: (Optional) Specify the filenames for the generated CIF composition and orchestration files. Defaults are Composition.cif and Orchestration.cif.
• -a: (Optional) Output intermediate contract automata (composition and orchestration).

Examples

1. Multiple Input Files: To compose a dealer and a player automaton and specify custom output names:

   java -jar CIF3Connector.jar -i Dealer.data Player.data -o MyComp.cif MyOrch.cif

2. Single Input File: If a single automaton is provided, it is treated as a pre-composed automaton. The tool will apply the most permissive controller synthesis before translating it to CIF3:

   java -jar CIF3Connector.jar -i CardComposition.data

Workflow Overview

When you run the tool with a list of principal contract automata, it performs the following internal steps:

1. Encode Lazy Transitions: Semi-controllable transitions are split into a pair consisting of one uncontrollable transition (internal selection) and one controllable transition (execution).
2. Composition & Synthesis: The tool utilizes CATLib to compose the automata and synthesizes the most permissive controller.
3. CIF3 Translation: The resulting composed automaton and the synthesized orchestration are translated into the textual .cif syntax, where final states are represented as marked states.

---

Note: This tool is part of the research presented in "Redundant Orchestration Synthesis for Contract Automata with CATLib and CIF3".