Corinne

This project presents an extension and improvement work by Corinne, a tool for reading, composing and projection of the Choreography Automata. These are an emerging model based on the concept of finite state automata mainly used for the top-down description of distributed systems choreographies. In particular, the project focuses on the implementation of the verification of Well-formedness, a fundamental characteristic of a c-automaton in order to ensure structural correctness, free from the typical errors of concurrent programming, such as Deadlocks and Race Conditions.

Table of Contents

• Dependencies
• Running
• Usage
• File List
• Author
• License

Dependencies

• Python3
• Graphviz (0.10.1)
• graphviz-python3-package (0.13.2)
• antlr4-python3-runtime (4.7.2)
• PIL (7.1.2)

Running

Open a terminal in the main folder of Corinne and type:

python3 main.py

Usage

• FILE MENU:

  • Open: takes in input DOT files (.gv) in CA syntax, but also it can get Chorgram file (.txt), a grammar used for Global Graph (See Chorgram) and DOT files (.gv) generated by Domitilla (See Domitilla)
    and convert them into DOT files with CA syntax.

  For more details about the CA syntax see DOT.g4 file.

  • Open saved tabs: opens previously saved without the need to open file already opened in other sessions

Once taken one or more files as input, Corinne can apply some functions on it, under the "Trasformations" or verify Well-formedness properties under the "Properties":

• TRASFORMATIONS:

  • Product: a cartesian product of two CA ;
  • Synchronization: given a CA, it can synchronize two particants of its ;
  • Projection: given a CA, you can select one participant from it and get the relative CFSM (Communicating-FSA)

• PROPERTIES:

  • Well-formedness: verify both the "Well-sequencedness" and "Well-branchedness" properties.
  • Well-sequencedness: verify only the "Well-sequencedness" property.
  • Well-branchedness: verify only the "Well-branchedness" property.

File List

• main.py : launch the program.
• guy.py : define the guy and its methods to create every view of the program.
• controller.py : define methods used by the guy to process files (open, render, ...).
• fsa.py : an abstract class to define a simple Finite State Machine and its methods.
• chor_auto.py : a class to define the Choreography Automata (CA), inherits from fsa class.
• cfsm.py : a class to define the Communicating FSA (CFSA), inherits from fsa class.
• dot_parser/* : contains the dot parser and every file it need to parse and convert.
• global_graph_parser/* : contains the Global Graph parser and every files it need to parse and convert.
• examples/* : some examples.
• well-formedness.py : define methods to verify well-formedness, well-branchedness and well-sequencedness.

Author

Main author:

Vairo Di Pasquale - vairodp - [email protected]

Other author(s):

Simone Orlando - simoneorlando - [email protected]

Ivan Lanese - lanese - [email protected]

License

This project is licensed under the MIT License - see the LICENSE file for details