Tutorial

Welcome to cyclone! Here are the tutorial we needed for learning the language. If you are already familiar with the language, feel free to try the editor.

This tutorial is a copy of the official tutorial. Contents may not be up to date.

0. Introduction

• 0.1 What is Cyclone ?

• 0.2 Installation

1. Fundamental

In this chapter, we will show you some of the basic features of Cyclone and solve some interesting problems in graph domain.

• 1.1 Understanding Cyclone's Specification Language

• 1.2 Finding Strings

• 1.3 Path Conditions

• 1.4 Finding Hamiltonian Path

• 1.5 Planning Route for an Agent

• 1.6 Summary

• 1.7 Path Operator Examples

• Exercise 1

• Exercise 2

2. Building Simple Models

In this chapter, we will show you features that you can use in Cyclone to solve problems from different domains such as test case generation,solution synthesis, program verification and model checking.

• 2.1 A Simple Counting Machine

• 2.2 Proving Zero-sum Game

• 2.3 Defuse a Bomb

• 2.4 Program Verification

• 2.5 Model a Hybrid System

• 2.6 Model Checking

• Exercise 1

• Exercise 2

3. Understanding Cyclone

In this chapter, we will introduce you some of the technical details about Cyclone. We hope this may help you to understand Cyclone better and eventually leads to thinking in Cyclone.

• 3.1 Variable Types

• 3.2 Operators

• 3.3 Assertions & Invariants

• 3.4 Conditional Transitions

• 3.5 Checking Modes

Appendix

• Language Reference

• Contributors