Component | Description |
---|---|
OS | Linux or macOS |
Processor | x86-64 |
Memory | 4 GiB or more |
gcc | 6.3 or later |
GTK+ | 3.x |
syncstitch
[
options …]
model-filename-x
process-name-b
-o
report-filename-n
num-workers-m
heap-size-t
hashtable-size-p
-v
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=****************
Syntax
(def
constant-name expression)
Example
(def N 4)
Syntax | Description |
---|---|
bool |
boolean (true or false ) |
(int a b) |
integer a ≤ k < b |
(set type) |
set of type |
(list type maxlen) |
list of type, maximum length is maxlen |
event |
event |
(channel type …) |
channel |
Syntax
(deftype
type-name { liteal | (
constructor type …)
} …)
Example
(deftype msg Req Can Ack Nak)
(deftype mutex-state Unlocked (Locked Pid))
Syntax
(deftypename
type-name type)
Example
(deftypename Pid (int 0 NumProcesses))
Syntax
(def (
function-name ((
parameter type)
…)
expression)
Example
(def (inc (k (int 0 4)))
(mod (+ k 1) 4))
Syntax
(defch
event-name)
(defch
channel-name type …)
Example
(defch e)
(defch ch (int 0 4) bool)
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))))
Syntax
STOP
CSP
STOP
Syntax
SKIP
CSP
SKIP
Syntax
(
process-name expression …)
Syntax
(!
event … process)
CSP
e -> P
Example
(! e P)
(! a b c P)
Remarks
(! a b c P)
= (! a (! b (! c P)))
Syntax
(?
channel (
parameter …)
[guard] process)
CSP
ch?x -> P(x)
Example
(? ch (x) (P x))
(? ch (k x) (= k j) (P x))
Syntax
(alt
process …)
CSP
P [] Q
Example
(alt P Q)
Note
(alt) = STOP
(alt
process)
= processSyntax
(amb
process …)
CSP
P |~| Q
(amb)
is ill-formed.
Syntax
(seq
process …)
CSP
P; Q
Note
(seq) = SKIP
(seq
process)
= processSyntax
(par
event-set process …)
CSP
P [|X|] Q
Example
(par (set a b) P Q)
Syntax
(hide
event-set process)
CSP
P \ X
Example
(hide (set a b) P)
Syntax
(rename
event-map process)
CSP
P[[R]]
chmap
.
Example
(rename (chmap (a b) (ch ch2)) Q)
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)
Syntax
(if
boolean-expression process process)
Example
(if (> x 0) P Q)
Syntax
(let (((
variable type)
expression)
…)
process)
Example
(let (((x (int 0 4)) (inc y))) (P x))
Syntax
(case
expression (
pattern expression)
…)
(
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)))
Syntax
true
false
Syntax
-2
, -1
, 0
, 1
, 2
, …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)
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.
Syntax
(
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))
Syntax
(
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.
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)
}
Syntax
(chmap (
event-or-channel event-or-channel)
…)
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))
(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
) }Syntax
(if
boolean-expression expression expression)
Syntax
(let (((
variable type)
expression)
…)
expression*)
(case
expression (
pattern expression)
…)
(
constructor parameter …)
Syntax
(type
type expression)
The operator type
coerces the type of expression to the type specified by type.
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.
Syntax
(executed
event)
@
event(executed-just
event)
^
eventexeucted
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.
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.
Syntax
(check (deadlock
P))
Check if the process P has a deadlock state or not.
Syntax
(check (divergence
P))
Check if the process P has a divergence or not.
Syntax
(check (traces
P Q))
Check if the process P is refined by the process Q on the traces semantics.
Syntax
(check (failures
P Q))
Check if the process P is refined by the process Q on the stable-failures semantics.
Syntax
(check (LTL
P formula))
Check if the process P satisfies the LTL formula formula or not.
(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)
Syntax
(check (CTL
process formula [fairness-assumption …]))
Check if the process P satisfies the CTL formula formula or not. fairness-assumptions are optional.
(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)
In CTL model checking, fairness assumptions can be specified. There are three types of 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.
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.
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.
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:
-x
option is specified with a process name in the model.Process Explorer consists of four panes.
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.
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.
Properties pane show the following properies of the selected state.
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.
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 |
(=
x y)
(not
x)
(and
x …)
(or
x …)
(<
x y)
(>
x y)
(<=
x y)
(>=
x y)
(+
x …)
(-
x)
(-
x y)
(*
x …)
(div
x y)
(mod
x y)
(expt
x n)
(mem
x collection)
(remove
collection x)
(list->set
xs)
(set->list
s)`(list
x …)
(null?
xs)
(length
xs)
(car
xs)
(cdr
xs)
(last
xs)
(butlast
xs)
(ref
xs k)
(take
xs 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)
(append1
xs x)
(append
xs …)
(update
xs k x)
(remove1
xs x)
(find-index
xs x)
(insert
xs k x)
(length
xs)
.
(remove-index
xs k)
(reverse
xs)
(interval
a b)
(make-list
n x)
(set
x …)
(empty?
s)
(subset?
s t)
(card
s)
(adjoin
s x …)
(union
s …)
(inter
s t …)
(diff
s t …)
(choice
s)