CAOS

CAOS is a framework to support computer aided design of structural operational semantics for formal models.

The framework is written in Scala 3 and can be imported as a submodule of any Scala project. It can be used to produce interactive visualisations of formal models under development, by compiling into JavaScript (using Scala.js) to be interpreted by a browser.

Requirements

• Scala version 2.13 or higher (to work with Scala 3)
• Scala building tools (sbt)
• Java Runtime Environment (JRE)

Using CAOS

CAOS is meant to be imported by an ongoing Scala project with a concrete Abstract Syntax Tree. The best way to learn how to use it is to follow examples of projects that use CAOS.

Examples of such projects include:

• Simple While-language (source)
• Simple Lambda Calculus (source)
• Ceta: Choreographic Extended Team Automata – realisability experiments (ICTAC'23 paper+source)
• Branching Pomset Encoder (ICE'22 paper+source)
• Pompset: Scala API generation of MPST via Pomsets (ECOOP'22 paper+source)
• ST4MP: Session Types for Multilanguage Programming (ISoLA'22 paper+source)
• Choreo: experiments with choreographies with strong choice and loops (source)
• Mars: early experiments on a language to generate runtime monitors (RTSS'20 short paper)
• Marx: experimental reactive language for synchronous architectures (source)
• VVML: animator and analyser of a subset of UML Activity Diagrams (source)
• Apoo: animator of a simple assembly language (Apoo's main page)
• CCS: animator of Milner's Calculus of Communicating Systems (source)
• MARGe: Animator of Labelled Reactive Graphs (source)

Alternatively, it is possible to start from a CAOS template, following the instructions described here (this template uses an older version of CAOS).

Tutorial on CAOS

The rest of this document describes the essentials needed to use CAOS. A more detailed tutorial can be found online:

• Caos' tutorial: https://arxiv.org/abs/2304.14901
• Caos' demo video: https://youtu.be/Xcfn3zqpubw

It is also possible to start with a simple template using giter8, based on a CCS example, by running sbt in the command line as follows.

sbt new arcalab/caos.g8

This command will automatically create a project structure with a minimal example that compiles, using a given name for the project.

Importing CAOS

We recommend to define CAOS as a git submodule of your own Scala project. Under your project folder run the following command.

git submodule add https://github.com/arcalab/CAOS.git lib/caos

This will add CAOS as a new git submodule into a folder lib/caos/.

Assuming you have a project named rootProject with the following build.sbt:

lazy val rootProject = project.in(file("."))
  .settings(
    name := "rootProject",
    scalaVersion := <yourversion>, // 2.13 or higher
    ...,
    libraryDependencies ++= Seq(
        ...
    )
  )

you can import and set CAOS by adding the following definitions:

lazy val caos = project.in(file("lib/caos"))
  .enablePlugins(ScalaJSPlugin)
  .settings(scalaVersion := "3.1.1")

lazy val rootProject = project.in(file("."))
    .settings(
        name := "rootProject",
        scalaVersion := <yourversion>, // 2.13 or higher
        ...,
        scalaJSUseMainModuleInitializer := true,
        // replace rootProject.Main by the correct path to your Main.scala class
        Compile / mainClass := Some("my.root.project.Main"),
        Compile / fastLinkJS / scalaJSLinkerOutputDirectory := 
            baseDirectory.value / "lib" / "caos"/ "tool" / "js" / "gen",
        libraryDependencies ++= Seq(
            ...,
        )
  ).dependsOn(caos)

Note that the scalaVersion of your project should typically match the one of CAOS.

You will also need to add the plugin for ScalaJS by appending to the file project/plugins.sbt (create file if it does not exist yet):

addSbtPlugin("org.scala-js" % "sbt-scalajs" % "1.7.1")

Instantiating CAOS

CAOS provides an interface (formally a trait in Scala) called Configurator:

// CAOS Configurator 

trait Configurator[Stx]:
  ///// Interface of a configurator for CAOS /////
  /** Name of the project */
  val name: String
  /** Optional: name of the input language */
  def languageName: String
  /** How to create an AST from text */
  val parser: String=>Stx
  /** List of examples *//
  val examples: Iterable[(String,Stx)]
  /** Main widgets, on the right hand side of the screen */
  val widgets: Iterable[(String,WidgetInfo[Stx])]
  /** Secondary widgets, below the code */
  val smallWidgets: Iterable[(String,WidgetInfo[Stx])]=Nil

object Configurator:
  ///// Constructors for widgets //////
  // Visualisers:
  def view[Stx](viewProg:Stx=>String, typ:ViewType): WidgetInfo[Stx]
  def viewTabs[Stx](viewProgs:Stx=>List[(String,String)], typ:ViewType): WidgetInfo[Stx]
  def viewMerms[Stx](viewProgs:Stx=>List[(String,String)]): WidgetInfo[Stx]
  def viewWarn[Stx](viewProg:Stx=>String,typ: ViewType):WidgetInfo[Stx]

  // Animators:
  def steps[Stx,A,S](initialSt:Stx=>S, sos:SOS[A,S], viewProg:S=>String, typ:ViewType): WidgetInfo[Stx]
  def lts[Stx,A,S](initialSt:Stx=>S,sos:SOS[A,S],viewSt:S=>String,viewAct:A=>String,maxSt:Int=80): WidgetInfo[Stx]

  // Comparing semantics:
  def compare[Stx,S1,S2](comp:(S1,S2)=>String, t:ViewType, pre1:Stx=>S1, pre2:Stx=>S2): WidgetInfo[Stx]
  def compareBranchBisim[Stx,A,S1,S2](sos1:SOS[A,S1],sos2:SOS[A,S2],pre1:Stx=>S1,pre2:Stx=>S2): WidgetInfo[Stx]
  def compareTraceEq[Stx,A,S1,S2](sos1:SOS[A,S1],sos2:SOS[A,S2],pre1:Stx=>S1,pre2:Stx=>S2): WidgetInfo[Stx]
  
  // Mandatory checks (throw errors and return warnings):
  def check[Stx](a: Stx=>Seq[String]): WidgetInfo[Stx]

To use CAOS you need to instantiate the Configurator[A] trait, for example in a classe. For example, for a MyLanguage object you could define:

class MyConcreteConfigurator extends Configurator[MyLanguage]: 
    //...
    val widgets = List(
      "View parsed data" -> view(x=>x.toString , Text),
      "View pretty diagram" -> view(MyGraph.buildMermaid, Mermaid),
      "Run small-steps" -> lts(
        myBuildInitState, mySmallSOS, myPrintState, myPrintLabels),
      ...
    )

Currently we can visualise plain text and Mermaid diagrams. A full example can be found, e.g., in the configurator in Choreo's project.

Finally, you need to call from your Main class to the initSite mehtod in CAOS.

// Root Project Main class 
package my.root.project
import caos.frontend.Site.initSite

object Main {
  def main(args: Array[String]):Unit = {
    initSite[ConcretStx](ConcreteConfigurator)
  }
}

Compiling CAOS

In root project you need to run sbt to compile using ScalaJS's compiler:

sbt fastLinkJS

The resulting web page, already linked to the compiled JavaScript, can be found in lib/tool/index.html, if you imported CAOS, or in the select <tool_path>/index.html, if you used the CAOS template.