Commit 8d11ac66 authored by Marius Bozga's avatar Marius Bozga
Browse files

add property for toekn-ring example

parent 1b3be83d
/*
*
* IF-Toolset - Copyright (C) UGA - CNRS - G-INP
*
* by Marius - Iulian - Susanne - Laurent - Joseph
* Bozga - Ober - Graf - Mounier - Sifakis
*
* This software is a computer program whose purpose is to simulate,
* explore and model-check real-time systems represented using the IF -
* intermediate format - language. This software package contains
* sources, documentation, and examples.
*
* This software is governed by the CeCILL-B license under French law and
* abiding by the rules of distribution of free software. You can use,
* modify and/ or redistribute the software under the terms of the
* CeCILL-B license as circulated by CEA, CNRS and INRIA at the following
* URL "http://www.cecill.info".
*
* As a counterpart to the access to the source code and rights to copy,
* modify and redistribute granted by the license, users are provided
* only with a limited warranty and the software's author, the holder of
* the economic rights, and the successive licensors have only limited
* liability.
*
* In this respect, the user's attention is drawn to the risks associated
* with loading, using, modifying and/or developing or reproducing the
* software by the user in light of its specific status of free software,
* that may mean that it is complicated to manipulate, and that also
* therefore means that it is reserved for developers and experienced
* professionals having in-depth computer knowledge. Users are therefore
* encouraged to load and test the software's suitability as regards
* their requirements in conditions enabling the security of their
* systems and/or data to be ensured and, more generally, to use and
* operate it in the same conditions as regards security.
*
* The fact that you are presently reading this means that you have had
* knowledge of the CeCILL-B license and that you accept its terms.
*
*/
pure observer o1;
state wait #start ;
match output token();
nextstate done;
endstate;
state done #success ;
endstate;
endobserver;
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment