Table of Contents

1 Prerequisites

• Communicating Sequential Processes (CSP)
• Linear Time Logic (LTL)
• Computation Tree Logic (CTL)

2 System Requirements

3 Invoking SyncStitch

3.1 Command-line options

-x process-name

explore the process.

-b

generate Büchi automata in the Graphviz dot format.

-o report-filename

specify report filename.

-n num-workers

specify the number of workers for parallel checking. The default is 1.

-m heap-size

specifiy the size of heaps in GiB. The default is 1 GiB.

-t hashtable-size

specifiy the number of hashtable slots (not in bytes). The default is 4000037.

-p

show progress.

-v

show version.

4 License key and settings file

The license key is specified in the setting file $HOME/.cspv. You can also customize preferences in the file. These keys are all optional.

Example

DPI=144
fontsize=12
facename=monospace
darkmode=1
license=****************

5 Modeling language

5.1 Model elements

• Constants
• Types
• Functions
• Channels
• Processes
• Fluents
• Assertions

5.2 Constants

Syntax

Example

(def N 4)

5.3 Types

5.3.1 Basic types

5.3.2 Algebraic data type

Syntax

Example

(deftype msg Req Can Ack Nak)

(deftype mutex-state Unlocked (Locked Pid))

5.3.3 Type names (type aliases)

Syntax

Example

(deftypename Pid (int 0 NumProcesses))

5.4 Functions

Syntax

Example

(def (inc (k (int 0 4)))
  (mod (+ k 1) 4))

5.5 Channels

Syntax

Example

(defch e)

(defch ch (int 0 4) bool)

5.6 Processes

5.6.1 Process definitions

Syntax

Example

(def P (! e STOP))

(def (P (s (set (int 0 4))))
  (? ch (x) (P (adjoin s x))))

5.6.2 STOP

Syntax

CSP

5.6.3 SKIP

Syntax

CSP

5.6.4 Process Calls

Syntax

5.6.5 Prefix

Syntax

CSP

Example

(! e P)

(! a b c P)

Remarks

5.6.6 Channel receive

Syntax

CSP

Example

(? ch (x) (P x))

(? ch (k x) (= k j) (P x))

5.6.7 Alternatives (external choice)

Syntax

CSP

Example

(alt P Q)

Note

5.6.8 Non-deterministic choice (internal choice)

Syntax

CSP

Note

at least one process is required, which means (amb) is ill-formed.

5.6.9 Sequential composition

Syntax

CSP

Note

5.6.10 Parallel composition

Syntax

CSP

Example

(par (set a b) P Q)

Note

at least two processes are required.

5.6.11 Hiding (concealment)

Syntax

CSP

Example

(hide (set a b) P)

5.6.12 Renaming

Syntax

CSP

Note

event-map is a map from events to events, which can be constructed with chmap.

Example

(rename (chmap (a b) (ch ch2)) Q)

5.6.13 Indexed operators

Indexed operators are folding forms of a sequence of processes for an operator. Four operators alt, amb, seq, and par have corresponding indexed-operators xalt, xamb, xseq, and xpar respectively.

They commonly have three components: parameter and its type, range, and process. xalt, xamb, and xseq are of the following form:

where xop is one of the three operators.

xpar is of the form:

This form indicates the process which is the result of folding a sequence of processes by the operator corresponding to xop. The sequence of processes is obtained by enumerating the value in range and substituting it for the parameter in process. Either a set or a list can be used as a range except for xseq. xseq only takes a list as range.

For example,

In the case that range is an event-set, only the following forms are allowed:

5.6.14 if

Syntax

Example

(if (> x 0) P Q)

5.6.15 let

Syntax

Example

(let (((x (int 0 4)) (inc y))) (P x))

5.6.16 case

Syntax

The expression expression must be an expression which evaluates to a value of an algebraic data type defined with deftype. The branch which pattern matches to the value is selected, each parameter in the pattern is bound to the corresponding value, then the process process of the branch is executed.

Note that literals and constructors in the patterns must be exclusive and exhaustive. There is no “else” form.

Example

(def N 4)
(deftypename Pid (int 0 N))
(deftype mutex-state Unlocked (Locked Pid))

(def P
  ...
  (case state
    (Unlocked   WAKEUP)
    ((Locked p) (PROCEED p)))

5.7 Expressions

5.7.1 Boolean constants

Syntax

5.7.2 Integer constants

Syntax

5.7.3 Universal sets

Syntax

UNIV indicates a set of all elements belonging to a type which is infered in the context. In the case that the type cannot be infered, specify the type by using the type form.

event indicates a set of all events defined in the current model.

Type names defined with deftypename are regarded as the universal set which element type is equal to the type name. This is a shorthand notation of:

5.7.4 Function applications

Syntax

function-name must be a builtin function or a user-defined function.

Note that high-order functions are not supported, which implies partial application is not allowed.

5.7.5 Events and Channels

Syntax

For channels, partial application is allowed. For example, if a channel ch takes n parameters and k (< n) arguments are given, the expression indicates a channel which takes n - k parameters.

Example

(defch ch bool (int 0 4))

(? (ch b) (x) (P x))

5.7.6 Literals and Contructors of Algebraic Data Types

Syntax

Literals of algebraic data types are constants.

Constructors are regarded as functions, and a constructor itself is not an expression because high-order functions are not supported.

5.7.7 chset

Syntax

The chset special form indicates a set of all events belonging to the argument. You can mix events and channels of any types.

Example

(defch a)
(defch b)
(defch ch (int 0 3))
(def X (chset a b ch))

X = { a, b, (ch 0), (ch 1), (ch 2) }

5.7.8 chmap

Syntax

chmap constructs a map from events to events.

• If a pair of event-or-channels are both events, they are mapped.

• If a pair of event-or-channels are both channels, their types must coincide and each event belonging to the channels are mapped.

• If an event and a channel are paired, the event is mapped to each event in the channel. This is a one-to-many mapping.

• If a channel and an event are paired, each event in the channel is mapped to the event. This is a many-to-one mapping.

Example

(defch a)
(defch b)
(defch c (int 0 3))
(defch d (int 0 3))

5.7.9 if

Syntax

5.7.10 let

Syntax

5.7.11 case

5.7.12 type

Syntax

The operator type coerces the type of expression to the type specified by type.

5.8 Fluents

5.8.1 Fluents

Syntax

Fluents are boolean variables which value varies along with a trace of a process. They are used as atomic propositions in LTL and CTL model checking.

initiating-set and terminating-set are sets of events. If the current value of the fluent is false and an event in initiating-set occurs, the fluent becomes true. If the current value of the fluent is true and an event in terminating-set occurs, the fluent becomes false. Otherwise the value of the fluent is unchanged.

initial-value is optional. If not specified, the initial value is false.

The second syntax defines the set of fluents which is indexed with index of type. Generally, initiating-set, terminating-set, and initial-value depends on index.

Suppose the type I is defined as (int 0 3) and a and b are channels on I,

defines three fluents (p 0), (p 1), and (p 2). (p 0) becomes true when (a 0) occurs and becomes false when (b 0) occurs, and so on.

5.8.2 Executed fluents

Syntax

exeucted and executed-just are special forms of fluents.

• (executed event) becomes true when event occurs and becomes false when other event other than tau occurs. It can also be written as @event.

• (executed-just event) becomes true when event occurs and becomes false when other event including tau occurs. It can also be written as ^event.

5.8.3 Enabledness

Syntax

(enabled event) is an atomic proposition on a state which is true iff the state has an outgoing transition labelled with event. (enabled event) can also be written as :event.

5.9 Assertions

5.9.1 Assertion Categories

• Deadlock
• Divergence
• Refinement relation on traces
• Refinement relation on stable failures
• LTL (Linear Time Logic)
• CTL (Computation Tree Logic)

5.9.2 Deadlock

Syntax

Check if the process P has a deadlock state or not.

5.9.3 Divergence

Syntax

Check if the process P has a divergence or not.

5.9.4 Refinement relation on traces

Syntax

Check if the process P is refined by the process Q on the traces semantics.

5.9.5 Refinement relation on stable-failures

Syntax

Check if the process P is refined by the process Q on the stable-failures semantics.

5.9.6 Linear Time Logic (LTL)

Syntax

Check if the process P satisfies the LTL formula formula or not.

5.9.6.1 LTL formulae

5.9.7 Computation Tree Logic (CTL) model checking

Syntax

Check if the process P satisfies the CTL formula formula or not. fairness-assumptions are optional.

5.9.7.1 CTL formulae

5.9.7.2 Fairness assumptions

In CTL model checking, fairness assumptions can be specified. There are three types of fairness assumptions:

• Unconditional
• Strong
• Weak

5.9.7.2.1 Unconditional fairness assumptions

Syntax

If an unconditional fairness assumption is specified, only paths which satisfies the LTL formula (G (F formula)) are searched.

xunconditional is an indexed form of unconditional fairness assumptions. For each value in range, the fairness assumption formula is assumed in which index is replaced with the value.

5.9.7.2.2 Strong fairness assumptions

Syntax

If a strong fairness assumption (strong p q) is specified, only paths which satisfies the LTL formula (imp (G (F p)) (G (F q))) are searched.

xstrong is an indexed form of strong fairness assumptions.

5.9.7.2.3 Weak fairness assumptions

Syntax

If a weak fairness assumption (weak p q) is specified, only paths which satisfies the LTL formula (imp (F (G p)) (G (F q))) are searched.

xweak is an indexed form of weak fairness assumptions.

6 Process Explorer

Process Explorer is a graphical interactive tool on which you can explore the behavior of the process as a computation tree. Process Explorer opens in two cases:

• On the command line, -x option is specified with a process name in the model.
• A violation or a witness of an assertion is found

6.1 Panes

Process Explorer consists of four panes.

• Path pane (A)
• Transitions pane (B)
• Properties pane (C)
• Diagram pane (D)

6.1.1 Path pane

Path pane shows a path from the initial state of the process to the selected state on the diagram as a list of events. In the case of showing a witness of LTL or CTL model checking, propositions and acceptance marks (LTL only) are also shown.

If an event on the path is selected by clicking, the corresponding state on the diagram turns blue and the properties of the state is shown on the properties pane. The selection can be cancelled by pressing the escape key.

6.1.2 Transitions pane

Transitions pane shows the outgoing transitions from the selected state on the diagram. If a checkbox of a transition is checked, the correspoinding transition and the target state are reified on the diagram. If unchecked, the transition and the subtree of the target state is removed from the diaram.

Hidden events are marked with asterisk ’*’. The corresponding transition on the diagram is shown as dotted line.

6.1.3 Properties pane

Properties pane show the following properies of the selected state.

• The state structure (alt, seq, par, hide, rename)
• The values of the state variables
• The propositions (CTL and LTL)
• The subformulae (CTL)
• The state of the Büchi automaton (LTL)

6.1.4 Diagram pane

Diagram pane shows the behavior of the process as a computation tree.

States are indicated as boxes. The properties of the states are shown in the box. In the case of exploring a violation of refinement checking on stable-failures model, a box indicates a set of states which can be reached from the initial state with the same trace. In this case, the minimal acceptances of the state set is shown in the box.

Transitions are indicated as line segments between boxes with a event label. They connects the source state and the target state. In the case of internal transitions (labelled with tau or a hidden event), the line segment is shown as a dotted-line.

6.2 Operations

7 Builtin functions

7.1 Equivalence

(= x y)

return true iff x and y are equal.

7.2 Boolean

(not x)

return false if x true, otherwise true.

(and x …)

return true iff all of x … are true.

(or x …)

return false iff all of x … are false.

7.3 Integer

(< x y)

return true iff x < y

(> x y)

return true iff x > y

(<= x y)

return true iff x <= y

(>= x y)

return true iff x >= y

(+ x …)

return the sum of x …

(- x)

return 0 - x

(- x y)

return x - y

(* x …)

return x * …

(div x y)

return the quotient of x / y

(mod x y)

return the remainder of x / y

(expt x n)

return x to the n-th power

7.4 List and Set

(mem x collection)

return true iff x is a member of collection. collection must be a list or a set.

(remove collection x)

return the same type of collection which member is in collection and is not equal to x. When collection is a list, the order is preserved.

(list->set xs)

return a set which includes all members of xs.

(set->list s)`

return a list in which each member of s occurs exactly once. The order of elements is arbitrary.

7.5 List

(list x …)

return a list consisting of x …

(null? xs)

return true iff xs is the empty list.

(length xs)

return the length of the list xs.

(car xs)

return the car of xs. xs* must be non-nil.

(cdr xs)

return the cdr of xs. xs* must be non-nil.

(last xs)

return the last element of xs. xs must be non-nil.

(butlast xs)

return the prefix list other than the last element of xs. xs must be non-nil.

(ref xs k)

return the k-th element of xs.

(take xs k)

return the prefix list of xs which length is k. 0 ≤ k ≤ (length xs).

(drop xs k)

return the tail list of xs which length is (length xs) - k. 0 ≤ k ≤ (length xs).

(cons x xs)

return the list which car is x and cdr is xs.

(append1 xs x)

return the list which is the result of adding x to the tail of xs.

(append xs …)

return the list which is the result of appending xs …

(update xs k x)

return the list which is the result of replacing the k-th element of xs with x.

(remove1 xs x)

return the list which is the result of removing the first occurrence of x in xs. x must be in xs.

(find-index xs x)

return the index of the first occurrence of x in xs. If x in not xs, -1 is returned.

(insert xs k x)

return the list which is the result of inserting x at the position indicated by k in xs. 0 ≤ k ≤ (length xs).

(remove-index xs k)

return the list which is the result of removing the k-th element of xs.

(reverse xs)

return the reversed list of xs.

(interval a b)

return the list which elements are from a to b exclusive.

(make-list n x)

return the list which length is n and every elements is x.

7.6 Set

(set x …)

return the set which elemets are x …

(empty? s)

return true iff s is empty.

(subset? s t)

return true iff s is a subset of t.

(card s)

return the number of elemetns in s.

(adjoin s x …)

return the set which is the result of adding x … to s.

(union s …)

return the union of s …

(inter s t …)

return the intersection of s t …

(diff s t …)

return the difference set of s of t …

(choice s)

return an arbitrary element of s. s must be non-empty.