Cyclone: Reference

This page provides a quick reference to the Cyclone specification language.

Grammar Rules

Grammar rules (older version) for Cyclone can be viewed here.

Call graph of grammar rules can be viewed here

Keywords

Click the following keywords to learn more about Cyclone specification language.

abstract^#	assert^#	at^-	bool^#	char⁼
condition^#	const^#	check^#	edge^#	enum^#
enumerate#	final^#	for^#	fresh^#	function^#
goal^#	graph^#	int^#	initial^#	invariant^#
label^#	let^#	machine^#	node^#	normal^#
prev⁼	on^#	reach^#	real^#	start^#
state^#	stop^#	string⁼	trans^#	transition^#
via^#	where^#	with^#

^#: can be compiled by Cyclone.

⁼: implemented but cannot be compiled in the current version.

^-: reserved only.

Path Operators

Cyclone works with different kinds of path condition and finds the kinds of paths specified by users. In order to form path conditions for Cyclone to meet, one must use one or more following path operators to construct a valid path condition.

Compound Path Condition

One can build compound path conditions by using standard one or more of the following logical operators:

not (!)
and (&&)
or (||)
xor (^)

Path variables

One can store multiple path conditions into a single path variable that can be used in the condition statement. These variables can be created using let expressions.

Supported Operators

Currently, Cyclone supports a range of operators just like other programming languages. Please click here to see the details.

Interchangeable Keywords

Here are the keywords can be used interchangeably.

state/node	machine/graph
edge/trans/transition	on/label
condition/via/with	reach/stop

Options

A user can use different options to configure how Cyclone verifies a specification. The complete list of options is here.