SyncStitch 3 Reference
Revision 1.0
2019/06/14
PRINCIPIA Limited

Table of Contents

1 Prerequisites

2 System Requirements

Component Description
OS Linux or macOS
Processor x86-64
Memory 4 GiB or more
gcc 6.3 or later
GTK+ 3.x

3 Invoking SyncStitch

 syncstitch [options] model-filename

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.

Key Description
DPI Specify DPI (dot-per-inch) of the display.
fontsize Specify font size in point.
facename Specify font face name.
darkmode Set 1 if darkmode is preffered.
license Specify the license key.

Example

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

5 Modeling language

5.1 Model elements

5.2 Constants

Syntax

(def constant-name expression)

Example

(def N 4)

5.3 Types

5.3.1 Basic types

Syntax Description
bool boolean (true or false)
(int a b) integer ak < b
(set type) set of type
(list type maxlen) list of type, maximum length is maxlen
event event
(channel type) channel

5.3.2 Algebraic data type

Syntax

(deftype type-name { liteal | (constructor type)} …)

Example

(deftype msg Req Can Ack Nak)
(deftype mutex-state Unlocked (Locked Pid))

5.3.3 Type names (type aliases)

Syntax

(deftypename type-name type)

Example

(deftypename Pid (int 0 NumProcesses))

5.4 Functions

Syntax

(def (function-name ((parameter type)) expression)

Example

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

5.5 Channels

Syntax

(defch event-name)
(defch channel-name type)

Example

(defch e)
(defch ch (int 0 4) bool)

5.6 Processes

5.6.1 Process definitions

Syntax

(def process-name process)
(def (process-name ((parameter type)) process)

Example

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

5.6.2 STOP

Syntax

STOP

CSP

STOP

5.6.3 SKIP

Syntax

SKIP

CSP

SKIP

5.6.4 Process Calls

Syntax

process-name
(process-name expression)

5.6.5 Prefix

Syntax

(! eventprocess)

CSP

e -> P

Example

(! e P)
(! a b c P)

Remarks

(! a b c P) = (! a (! b (! c P)))

5.6.6 Channel receive

Syntax

(? channel (parameter) [guard] process)

CSP

ch?x -> P(x)

Example

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

5.6.7 Alternatives (external choice)

Syntax

(alt process)

CSP

P [] Q

Example

(alt P Q)

Note

(alt) = STOP
(alt process) = process

5.6.8 Non-deterministic choice (internal choice)

Syntax

(amb process)

CSP

P |~| Q
Note
at least one process is required, which means (amb) is ill-formed.

5.6.9 Sequential composition

Syntax

(seq process)

CSP

P; Q

Note

(seq) = SKIP
(seq process) = process

5.6.10 Parallel composition

Syntax

(par event-set process)

CSP

P [|X|] Q

Example

(par (set a b) P Q)
Note
at least two processes are required.

5.6.11 Hiding (concealment)

Syntax

(hide event-set process)

CSP

P \ X

Example

(hide (set a b) P)

5.6.12 Renaming

Syntax

(rename event-map process)

CSP

P[[R]]
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:

(xop (parameter type) range process)

where xop is one of the three operators.

xpar is of the form:

(xpar (parameter type) range event-set process)

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,

(xalt (i I) (set a b c) (P i)) = (alt (P a) (P b) (P c))

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

(xalt e event-set (! e process ))
(xamb e event-set process)

5.6.14 if

Syntax

(if boolean-expression process process)

Example

(if (> x 0) P Q)

5.6.15 let

Syntax

(let (((variable type) expression)) process)

Example

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

5.6.16 case

Syntax

(case expression (pattern expression))
  where pattern ::= literal | (constructor parameter)

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

true
false

5.7.2 Integer constants

Syntax

…, -2, -1, 0, 1, 2, …

5.7.3 Universal sets

Syntax

UNIV
event

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:

(type (set typename ) UNIV)

5.7.4 Function applications

Syntax

(function-name expression)

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

event
channel
(channel expression)

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

literal
(constructor expression)

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

(chset event-or-channel)

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 (event-or-channel event-or-channel))

chmap constructs a map from events to events.

Example

(defch a)
(defch b)
(defch c (int 0 3))
(defch d (int 0 3))
(chmap (a b)) = { (a, b) }
(chmap (c d)) = { ((c 0), (d 0)), ((c 1), (d 1)), ((c 2), (d 2)) }
(chmap (a c)) = { (a, (c 0)), (a, (c 1)), (a, (c 2)) }
(chmap (c a)) = { ((c 0), a), ((c 1), a), ((c 2), a) }

5.7.9 if

Syntax

(if boolean-expression expression expression)

5.7.10 let

Syntax

(let (((variable type) expression)) expression*)

5.7.11 case

(case expression (pattern expression))
where pattern ::= literal | (constructor parameter)

5.7.12 type

Syntax

(type type expression)

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

5.8 Fluents

5.8.1 Fluents

Syntax

(fluent fluent-name initiating-set terminating-set [initial-value])
(fluent (fluent-name (index type)) initiating-set terminating-set [initial-value])

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,

(fluent (p (i I)) (set (a i)) (set (b 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

(executed event)
@event
(executed-just event)
^event

exeucted and executed-just are special forms of fluents.

5.8.3 Enabledness

Syntax

(enabled event)
:event

(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

5.9.2 Deadlock

Syntax

(check (deadlock P))

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

5.9.3 Divergence

Syntax

(check (divergence P))

Check if the process P has a divergence or not.

5.9.4 Refinement relation on traces

Syntax

(check (traces P Q))

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 (failures P Q))

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 (LTL P formula))

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

5.9.6.1 LTL formulae

  formula ::=
       fluent
     | (enabled event)
     | (executed event)
     | (executed-just event)
     | (not formula)
     | (and formula)
     | (or formula)
     | (imp formula formula)
     | (forall index range formula)
     | (exists index range formula)
     | (X formula)
     | (F formula)
     | (G formula)
     | (U formula formula)
     | (W formula formula)
     | (R formula formula)
     | (M formula formula)

5.9.7 Computation Tree Logic (CTL) model checking

Syntax

(check (CTL process formula [fairness-assumption …]))

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

5.9.7.1 CTL formulae

  formula ::=
       fluent
     | (enabled event)
     | (executed event)
     | (executed-just event)
     | (not formula)
     | (and formula)
     | (or formula)
     | (imp formula formula)
     | (forall index range formula)
     | (exists index range formula)
     | (EX formula)
     | (EF formula)
     | (EG formula)
     | (EU formula formula)
     | (AX formula)
     | (AF formula)
     | (AG formula)
     | (AU formula formula)

5.9.7.2 Fairness assumptions

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

5.9.7.2.1 Unconditional fairness assumptions

Syntax

(unconditional formula)
(xunconditional index range formula)

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

(strong formula formula)
(xstrong index range formula formula)

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

(weak formula formula)
(xweak index set formula formula)

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:

6.1 Panes

Process Explorer consists of four panes.

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.

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

Operation Effects
Select a transition The properties of the target state is shown on the properties pane.
Check a transition The transition and the target state are reified on the diagram.
Uncheck a transition The transition, the target state and the subtree are removed.
Double-click a transition The transition and the target state are reified on the diagram and the target is selected.
Select an event on the path The corresponding state turns blue and its properies are shown on the properties pane.
Up/Down key Move the selection on the transition/path
Escape Unselect the transition / the event on the path.
Delete/Backspace Delete the selected state and the subtree.
Right-Drag Scroll view diagram (move view position)
Alt + Click Select a subtree.
Shift + Click Add to/Remove from the selection.
Control + Wheel Zoom in/out.
Control + E Expand all transitions (check all).
Control + J Fit the size of the selected state to the contents.
Control + Z Undo.
Control + Y Redo.
Control + U Bring the selected state to front.
Control + D Push back the selected state.
Control + L Adjust the view position.
Control + R Move view position to the right most state.
Control + 0 Reset view position and zoom ratio.
Control + P Save the diagram as PDF and SVG
Control + W Quit Process Explorer
Control + Q Quit Process Explorer

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.