JSON API

Table of Contents

1. Main Types
   1. Linear Propositions linprop
   2. Annotated terms linterm
   3. Composition actions action
   4. Provenance prov
   5. Provenance entries prov_entry and iprov_entry
   6. Action state actionstate
   7. Agent agent
   8. Process process
2. Commands
   1. Ping
   2. Create
   3. Binary compose (compose1)
   4. Compose
   5. Verify
   6. Deploy
3. Responses
   1. Pong
   2. Create
   3. Compose
   4. Verify
   5. Deploy
   6. Failed
   7. Exception

Main Types

Linear Propositions linprop

Description

Linear terms are either:

1. atoms
2. subterms connected by tensor or plus
3. negations of terms

Structure

• type: string = "var" | "neg" | "times" | "plus"
• name: string = the name of the atom if type = "var", otherwise ignored
• args: array of linprop = the list of arguments if type is neg, times or plus, otherwise ignored. Binary operators times and plus can have more than 2 arguments, in which case they are applied in a right associative way

Annotated terms linterm

Description

Annotated terms are linear propositional terms annotated with a channel.

Structure

• cll: linprop
• channel: string

Composition actions action

Description

Composition actions describe a binary combination of 2 labelled processes.

Structure

• act: string = the type of composition, currently "JOIN" | "TENSOR" | "WITH" for sequential, parallel, and conditional composition respectively
• larg: string = the name of the first (or “left”) component process
• lsel: string = a string describing some relevant part of the left process component. This is different depending on the action type.
• rarg: string = the name of the second (or “right”) component process
• rsel: string = a string describing some relevant part of the right process component. This is different depending on the action type.
• res: string = the desired label for the resulting composition

[TODO] Selections are expected as follows:

• TENSOR:
• WITH:
• JOIN:

Provenance prov

Description

Provenance trees are used to determine the origin of each linear proposition in an input or output term.

For example, consider 2 processes:

• P with input X and output A ** B
• Q with inputs B and Y and output C

These can be joined through B. The resulting composition will have inputs X and Y and output A ** C. In this the following hold:

• X has an input provenance of P
• Y has an input provenance of Q
• In the output, A comes from P and C comes from Q so we construct the JSON object "P ** Q"

The structure of the provenace tree matches the syntax tree of the corresponding term. For this reason with copy the structure of linprop but use the name to record the provenance label instead of the atom name.

Subtrees where all propositions have the same provenance can be replaced by an atomic/leaf provenance node with the single label. This is the only exception of the provenance tree not matching the syntax tree.

Structure

• type: string = "source" | "times" | "plus"
• name: string = the provenance label if type = "source", otherwise ignored
• args: array of prov = the list of arguments if type is times or plus, otherwise ignored. Binary operators times and plus can have more than 2 arguments, in which case they are applied in a right associative way

[TODO: clarify provenance labels]

Provenance entries prov_entry and iprov_entry

Description

Provenance info is kept in the state. Provenance entries associate a provenance tree to the output (prov_entry) or input (iprov_entry) it corresponds to. Output provenance is associated with a process label whose output it describes. Input provenance is associated with an available input term.

[TODO: clarify]

*In the future, provenance info will be kept directly in the process instead of the state.- This will make thing a bit more intuitive.

Structure

prov_entry:

• name: string = the name/label of the process whose output we are describing
• prov: prov = the corresponding provenance tree

iprov_entry:

• term: linprop = the (non-negated) linear term of the input we are describing
• prov: prov = the corresponding provenance tree

Action state actionstate

Description

The action state is used to convey state info to the prover and retrieve proof metadata afterwards.

Structure

• label: string = a unique label identifying the composite process under contruction
• ctr: int = a non-negative counter used to keep variables fresh. Expected to be initialized to 0.
• buffered: array of linprop = the types of buffers that were constructed during proof. This used to be the way to determine buffered edges in the frontend, but is now obsolete thanks to the provenance trees.
• joined: array of linterm = the inputs that were used up/connected during a JOIN action.
• iprov: array of iprov_entry = input povenance entries
• prov: array of prov_entry = output provenance entries

Agent agent

An agent refers to a pi-calculus agent corresponding to a process specification. Currently this is just a string, but we have plans to adopt a more structured representation in the near future.

Process process

Description

The complete specification of a process.

Structure

• name: string = a name/label for the process
• inputs: array of linterm
• output: linterm
• prov: prov = the output provenance
• proc: agent = the pi-calculus specification
• actions: array of action = a list of composition actions that construct this process. Empty if the process is atomic.
• copier: bool = true if the prover determines this to be a copy node
• intermediate: bool = true if this is an intermediate composition step (as opposed to an atomic process or completed composition)

Commands

All commands include a command field of type string which defines the type of the command.

Ping

Description

Ping/keep-alive command. Gives a Pong response.

Structure

• command: string = "ping"
• ping: float = a timestamp to measure ping

Create

Description

A command to create a new atomic process.

Structure

• command: string = "create"
• name: string = the name of the process to be created
• inputs: array of linprop = a list of inputs. Their channels will be created by the prover.
• output: linprop = the process output. The channcel will be created by the prover.

Binary compose (compose1)

Description

Binary composition of 2 processes with a single action.

Although a more general composition command is provided, when it comes to simple binary compositions this command executes faster.

Structure

• command: string = "compose1"
• action: action = the composition action to be performed. The labels of the 2 arguments must match the labels of the processes provided in the next fields.
• lhs: process = the process corresponding to the first (left) argument of the action
• rhs: process = the process corresponding to the second (right) argument of the action

Compose

Description

Construction of a complex composition with one or more actions. Although more general than the binary composition command compose1, it is slower.

Structure

• command: string = "compose"
• name: string = the name of the final composition
• components: array of process = the list of all component processes that will be used
• actions: array of action = the ordered list of actions to be performed

Verify

Description

A command used to reconstruct a process composition.

This is legacy command which has now devolved into the compose command. The only difference is that verify does not produce compose responses for intermediate steps. It will only generate one verify response for the final process.

Structure

• command: string = "verify"
• name: string = the name of the final composition
• components: array of process = the list of all component processes that will be used
• actions: array of action = the ordered list of actions to be performed

Deploy

Description

This is a family of commands that produce executable process deployments.

There are currently 3 types of possible deployments:

1. PiViz: This produces a file for the PiVizTool and/or MWB.
2. PiLib: This produces a deployment and code templates using the old PiLib library.
3. PEW: This produces a deployment and code templates with the newer PEW library.

Structure

1. PiViz

   • command: string = "piviz"
   • process: process = the process to be deployed
   • components: array of process = the list of all dependencies/components required in the composition

2. PiLib

   • command: string = "pilib"

   • process: process = the process to be deployed

   • components: array of process = the list of all dependencies/components required in the composition

   • separator: string = the client OS-specific file path separator

   • path: string = the base path for the deployment

   • pkg: string = the desired name for the Scala package that will contain the code

   • project: string = an identifiable name for the deployment. This will be used to identify certain types and classes.

   • main: bool = true if the generation of a template for a main class is required.

   • java: bool = true if the generation of a java runner class is required. This can help integrate the Scala deployment with Java code.

3. PEW

   • command: string = "piviz"

   • process: process = the process to be deployed

   • components: array of process = the list of all dependencies/components required in the composition

   • separator: string = the client OS-specific file path separator

   • path: string = the base path for the deployment

   • pkg: string = the desired name for the Scala package that will contain the code

   • project: string = an identifiable name for the deployment. This will be used to identify certain types and classes.

   • main: bool = true if the generation of a template for a main class is required.

   • java: bool = true if the generation of a java runner class is required. This can help integrate the Scala deployment with Java code.

Responses

All responses include a response field of type string which defines the type of the response.

Pong

Description

The response to the Ping command.

Structure

• response: string = "Pong"
• ping: float = contains the original timestamp received by the prover in the Ping command.

Create

Description

The response to the create command with a definition of a new atomic process.

Structure

• response: string = "CreateProcess"
• process: process = the newly created process

Compose

Description

The result of a single binary composition action. The compose command may produce multiple of these, one for each action.

Structure

• response: string = "Compose"
• action: action = the composition action that was applied
• process: process = the resulting composite process
• state: actionstate = the updated action state with the associated metadata

Verify

Description

The response of the verify command with a reconstructed composite process.

Structure

• response: string = "Verify"
• process: process = the reconstructed composition

Deploy

Description

This is the response to the deploy commands. It describes the files that are required for deployment.

Structure

First we need the structure for a single deployment file. This is a file object containing the following fields:

• path: string = the full path of the file (including its name) in the deployment
• content: string = the content of the file
• overwrite: bool = the reasoner tags the files that are generated fully automatically so that they will be overwritten in consecutive deployments. Files that may be edited by the user (e.g. code templates) have this field marked as false to avoid overwritting user content.

Based on this, the deploy response is as follows:

• response: string = "Deploy"
• type: string = the type of deployment. Currently one of PiViz, PiLib or PEW.
• deployment: Array of file = a list of deployment files.

Failed

Description

This response is generated whenever the prover fails to perform a command. Unless there is a bug or associated limitation in the prover, this indicates a user or input error.

Structure

• response: string = "CommandFailed"
• content: string = a (sometimes useful) description of the error that occured

Exception

Description

This response is generated whenever the prover fails due to an internal exception. This indicates an expected failure in the system.

Structure

• response: string = "Exception"
• content: string = the contents of the thrown exception