Calculus of Communicating Systems

Introduction

The Calculus of Communicating Systems (CCS) is a process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus.
Its actions model indivisible communications between exactly two participants.
The formal language includes primitives for describing parallel composition, the choice between actions and scope restriction.
CCS is useful for evaluating the qualitative correctness of properties of a system such as a deadlock or livelock.

Description

This program calculates the abstract tree of the computation performed by the rules of the Calculus of Communicating Systems created by Robin Milner.
You can print the abstract tree.
For more information about Calculus of Communication System
You can find more information in the pdf file.
Assigned by Professor Pietro Cenciarelli at University of Rome Sapienza during the course Programming Languages and Types Theory.

An example is:

 _ --> (a!.0 | (c?.0 + b!.0))
   !a --> (0 | (c?.0 + b!.0))
      _ --> (0 | c?.0)
         ?c --> (0 | 0)
      _ --> (0 | b!.0)
         !b --> (0 | 0)
   _ --> (a!.0 | c?.0)
      ?c --> (0 | a!.0)
         !a --> (0 | 0)
      !a --> (c?.0 | 0)
         ?c --> (0 | 0)
   _ --> (a!.0 | b!.0)
      !a --> (0 | b!.0)
         !b --> (0 | 0)
      !b --> (a!.0 | 0)
         !a --> (0 | 0)

Getting Started

These instructions will get you a copy of the project up and running on your local machine for development and testing purposes. See deployment for notes on how to deploy the project on a live system.

Prerequisites

You must be able to run .sml files (Standard ML of New Jersey).

• You can install from smlnj.org the SML compiler it's available for UNIX & Windows System. After the installation

     $ sml ccs.sml 

• Otherwise, you can execute it in the online compiler on the website by copying it to it and then pressing the play button.

Running the tests

To run a test, use this synopsis. Example:

; val programExample = Par (
    Output_proc ("a", Empty_proc),
    Or (Input_proc ("a", Empty_proc), Output_proc ("a", Empty_proc))
    )

; (print or tree_to_string or eval_ccs) programExample

example of result

The form of the parameters is specified in the abstract algebra:

; datatype process = Empty_proc
    | Input_proc of channel * process
    | Output_proc of channel * process
    | Or of process * process
    | Par of process * process

Authors

• Alessandro Scandone - Github profile
• Andrea Bacciu Github profile
• Valerio Neri Github profile

See also the list of contributors who participated in this project.

License

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