forked from yzh89/MITL2Timed
-
Notifications
You must be signed in to change notification settings - Fork 0
Modifying Oddoux and Gastin's ltl2ba (http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/) to perform Transformation from Metric Interval Temporal Logic to Timed Automata
License
barbosafs/MITL2Timed
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
MITL2Timed - transforms a MITL formula to a timed automaton based on LTL2BA. Forked from https://github.com/slivingston/ltl2gba. Modified by Yuchen Zhou, University of Maryland, USA. Copyright (c) 2015 Yuchen Zhou Available at https://github.com/yzh89/MITL2ta 1. LICENSE OF LTL2BA LTL2BA - Version 1.0 - October 2001 Written by Denis Oddoux, LIAFA, France Copyright (c) 2001 Denis Oddoux LTL2BA - Version 1.1 - August 2007 Modified by Paul Gastin, LSV, France Copyright (c) 2007 Paul Gastin Available at http://www.lsv.ens-cachan.fr/~gastin/ltl2ba Modified by Scott C. Livingston, Caltech, USA. Copyright (c) 2013 Scott C. Livingston Available at https://github.com/slivingston/ltl2gba. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. GNU GPL is included in this distribution, in a file called 'LICENSE' This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA The LTL2BA software was written by Denis Oddoux and modified by Paul Gastin. It is based on the translation algorithm presented at CAV '01: P.Gastin and D.Oddoux "Fast LTL to Büchi Automata Translation" in 13th International Conference on Computer Aided Verification, CAV 2001, G. Berry, H. Comon, A. Finkel (Eds.) Paris, France, July 18-22, 2001, Proceedings - LNCS 2102, pp. 53-65 Send bug-reports and/or questions to Paul Gastin http://www.lsv.ens-cachan.fr/~gastin Part of the code included is issued from the SPIN software Version 3.4.1 The SPIN software is written by Gerard J. Holzmann, originally as part of ``Design and Validation of Protocols,'' ISBN 0-13-539925-4, 1991, Prentice Hall, Englewood Cliffs, NJ, 07632 Here are the files that contain some code from Spin v3.4.1 : cache.c (originally tl_cache.c) lex.c ( tl_lex.c ) ltl2ba.h ( tl.h ) main.c ( tl_main.c ) mem.c ( tl_mem.c ) parse.c ( tl_parse.c) rewrt.c ( tl_rewrt.c) trans.c ( tl_trans.c) 2. Changes for MITL2Timed Main changes is the addition of file timed.c to create the timed automata based on MITL. parse.c and trans.c is modified according to parse the input and generate the output correctly. Additional python scripts are generated alone the way to create UPPAAL models for model checking. 3. COMPILING compile the program > make 4. EXECUTING (for MITL2Timed) run the program > ./mitl2ta -f "formula" The formula is an MITL formula, and may contain propositional symbols, boolean operators, temporal operators, and parentheses. The syntax used is the one used in the 'Spin' model-checker Propositonal Symbols: true, false any lowercase string Boolean operators: ! (negation) -> (implication) <-> (equivalence) && (and) || (or) Temporal operators: [] (always) <> (eventually) U (until) V (release) X (next) <>_[l,r] (eventually with interval l to r) []_[l,r] (always with interval l to r) Use spaces between any symbols. 5. Map information is hard coded at current stage. The robot can move up or down and right or left if there is any. It can be easily extends to larger grid. pos0 pos1:b pos2:a pos3
About
Modifying Oddoux and Gastin's ltl2ba (http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/) to perform Transformation from Metric Interval Temporal Logic to Timed Automata
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published
Languages
- C 98.6%
- Other 1.4%