/dports/math/spot/spot-2.10.2/doc/org/ |
H A D | tut01.org | 2 #+TITLE: Parsing and Printing LTL Formulas 14 Using =ltlfilt=, you can easily read an LTL formula in one syntax, and 102 type of formula they can output. Here we are only using LTL formulas 139 Note that as its name implies, this parser can read more than LTL 140 formulas: the fragment of PSL we support is basically LTL extended 231 ** PSL vs LTL 237 you can simply use =parse_infix_psl()= to parse LTL formulas. 274 The first is to simply diagnose non-LTL formulas. 291 std::cerr << "Only LTL formulas are supported.\n"; 326 std::cerr << "Only LTL formulas are supported.\n"; [all …]
|
H A D | index.org | 2 #+TITLE: Spot: a platform for LTL and ω-automata manipulation 3 #+DESCRIPTION: Spot is a library and tool suite for LTL and ω-automata 4 #+KEYWORDS: Spot,C++17,library,platform,framework,tool-suite,LTL,PSL,omega-automata 8 Spot is a C++17 library for LTL, ω-automata manipulation and model 11 - Support for [[file:concepts.org::#ltl][LTL]] (several syntaxes supported) and 34 conditions. It can be used to test tools that translate LTL into 54 …s://spot.lrde.epita.fr/app/][Our on-line translator]] provides a convenient way to translate LTL or
|
H A D | tut.org | 23 - [[file:tut01.org][Parsing and Printing LTL Formulas]] 25 - [[file:tut04.org][Testing the equivalence of two LTL formulas]] 26 - [[file:tut10.org][Translating an LTL formula into a never claim]] 27 - [[file:tut11.org][Translating an LTL formula into a monitor]] 28 - [[file:tut12.org][Working with LTL formulas with finite semantics]] 61 - [[https://spot.lrde.epita.fr/ipynb/formulas.html][=formulas.ipynb=]] covers the basics of LTL/PSL… 77 …ipynb/synthesis.html][=synthesis.ipynb=]] illustrates support for game-based LTL reactive synthesis 81 - [[https://spot.lrde.epita.fr/ipynb/gen.html][=gen.ipynb=]] show how to generate families of LTL f…
|
H A D | ltlsynt.org | 3 #+DESCRIPTION: Spot command-line tool for synthesizing AIGER circuits from LTL/PSL formulas. 10 This tool synthesizes controllers from LTL/PSL formulas. 27 - =--formula= or =--file=: a specification in LTL or PSL. 105 …b.com/reactive-systems/syfco][=syfco=]] which can translate a TLSF specification to an LTL formula. 111 LTL=$(syfco FILE -f ltlxba -m fully) 114 ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT" 124 LTL decomposition consist in splitting the specification into multiple 185 The initial reduction from LTL to parity game is described in the 188 - *Reactive Synthesis from LTL Specification with Spot*, /Thibaud Michaud/,
|
H A D | tut12.org | 2 #+TITLE: Working with LTL formulas with finite semantics 10 The LTL operators used by Spot are defined over infinite words, and 20 build a finite automaton that recognize some LTLf (i.e. LTL with 23 1. Have Spot read the input LTLf formula as if it was LTL. 25 LTL. First, introduce a new atomic proposition =alive= that will 27 Then adjust all original LTL operators so that they have to be 57 paper]]. However, beware that the LTLf to LTL rewriting suggested in 66 executed as follows. Transforming LTLf to LTL can be done using 113 LTL and translate the result into a Büchi automaton using
|
H A D | ioltl.org | 2 #+TITLE: Common input and output options for LTL/PSL formulas 8 Spot supports different syntaxes for LTL/PSL formulas. This page 14 All tools that read LTL/PSL formulas implement the following options: 49 Spot's default LTL parser is able to parse the syntaxes of many tools, 62 Spot's default LTL parser will understand all of them. 71 the LTL formula =G(F(a))=. Any double-quoted string is also 87 in LTL formulas. The previous formula would be written simply: 96 first tries to recursively parse the block as an LTL/PSL formula, and 101 For instance =(a U b) U c= will be successfully converted into an LTL 269 in LTL formulas), but you can use =xargs -0= to split the input on [all …]
|
/dports/math/py-spot/spot-2.10.2/doc/org/ |
H A D | tut01.org | 2 #+TITLE: Parsing and Printing LTL Formulas 14 Using =ltlfilt=, you can easily read an LTL formula in one syntax, and 102 type of formula they can output. Here we are only using LTL formulas 139 Note that as its name implies, this parser can read more than LTL 140 formulas: the fragment of PSL we support is basically LTL extended 231 ** PSL vs LTL 237 you can simply use =parse_infix_psl()= to parse LTL formulas. 274 The first is to simply diagnose non-LTL formulas. 291 std::cerr << "Only LTL formulas are supported.\n"; 326 std::cerr << "Only LTL formulas are supported.\n"; [all …]
|
H A D | index.org | 2 #+TITLE: Spot: a platform for LTL and ω-automata manipulation 3 #+DESCRIPTION: Spot is a library and tool suite for LTL and ω-automata 4 #+KEYWORDS: Spot,C++17,library,platform,framework,tool-suite,LTL,PSL,omega-automata 8 Spot is a C++17 library for LTL, ω-automata manipulation and model 11 - Support for [[file:concepts.org::#ltl][LTL]] (several syntaxes supported) and 34 conditions. It can be used to test tools that translate LTL into 54 …s://spot.lrde.epita.fr/app/][Our on-line translator]] provides a convenient way to translate LTL or
|
H A D | tut.org | 23 - [[file:tut01.org][Parsing and Printing LTL Formulas]] 25 - [[file:tut04.org][Testing the equivalence of two LTL formulas]] 26 - [[file:tut10.org][Translating an LTL formula into a never claim]] 27 - [[file:tut11.org][Translating an LTL formula into a monitor]] 28 - [[file:tut12.org][Working with LTL formulas with finite semantics]] 61 - [[https://spot.lrde.epita.fr/ipynb/formulas.html][=formulas.ipynb=]] covers the basics of LTL/PSL… 77 …ipynb/synthesis.html][=synthesis.ipynb=]] illustrates support for game-based LTL reactive synthesis 81 - [[https://spot.lrde.epita.fr/ipynb/gen.html][=gen.ipynb=]] show how to generate families of LTL f…
|
H A D | tut12.org | 2 #+TITLE: Working with LTL formulas with finite semantics 10 The LTL operators used by Spot are defined over infinite words, and 20 build a finite automaton that recognize some LTLf (i.e. LTL with 23 1. Have Spot read the input LTLf formula as if it was LTL. 25 LTL. First, introduce a new atomic proposition =alive= that will 27 Then adjust all original LTL operators so that they have to be 57 paper]]. However, beware that the LTLf to LTL rewriting suggested in 66 executed as follows. Transforming LTLf to LTL can be done using 113 LTL and translate the result into a Büchi automaton using
|
H A D | ltlsynt.org | 3 #+DESCRIPTION: Spot command-line tool for synthesizing AIGER circuits from LTL/PSL formulas. 10 This tool synthesizes controllers from LTL/PSL formulas. 27 - =--formula= or =--file=: a specification in LTL or PSL. 105 …b.com/reactive-systems/syfco][=syfco=]] which can translate a TLSF specification to an LTL formula. 111 LTL=$(syfco FILE -f ltlxba -m fully) 114 ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT" 124 LTL decomposition consist in splitting the specification into multiple 185 The initial reduction from LTL to parity game is described in the 188 - *Reactive Synthesis from LTL Specification with Spot*, /Thibaud Michaud/,
|
H A D | ioltl.org | 2 #+TITLE: Common input and output options for LTL/PSL formulas 8 Spot supports different syntaxes for LTL/PSL formulas. This page 14 All tools that read LTL/PSL formulas implement the following options: 49 Spot's default LTL parser is able to parse the syntaxes of many tools, 62 Spot's default LTL parser will understand all of them. 71 the LTL formula =G(F(a))=. Any double-quoted string is also 87 in LTL formulas. The previous formula would be written simply: 96 first tries to recursively parse the block as an LTL/PSL formula, and 101 For instance =(a U b) U c= will be successfully converted into an LTL 269 in LTL formulas), but you can use =xargs -0= to split the input on [all …]
|
/dports/math/spot/spot-2.10.2/bin/man/ |
H A D | ltlsynt.x | 3 ltlsynt \- reactive synthesis from LTL specifications 10 Thibaud Michaud, Maximilien Colange: Reactive Synthesis from LTL
|
H A D | randltl.x | 2 randltl \- generate random LTL/PSL formulas 10 Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0.
|
H A D | ltl2tgba.x | 3 ltl2tgba \- translate LTL/PSL formulas into Büchi automata 159 Because of this limited expressiveness, a monitor for some given LTL 161 the formula. For instance a monitor for the LTL formula \f(CWa U b\fR 194 improvements to LTL translation. Proceedings of SPIN'13. LNCS 7976.
|
/dports/math/py-spot/spot-2.10.2/bin/man/ |
H A D | randltl.x | 2 randltl \- generate random LTL/PSL formulas 10 Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0.
|
H A D | ltlsynt.x | 3 ltlsynt \- reactive synthesis from LTL specifications 10 Thibaud Michaud, Maximilien Colange: Reactive Synthesis from LTL
|
H A D | ltl2tgba.x | 3 ltl2tgba \- translate LTL/PSL formulas into Büchi automata 159 Because of this limited expressiveness, a monitor for some given LTL 161 the formula. For instance a monitor for the LTL formula \f(CWa U b\fR 194 improvements to LTL translation. Proceedings of SPIN'13. LNCS 7976.
|
/dports/math/gsl/gsl-2.7/multifit/ |
H A D | test_reg.c | 284 gsl_matrix *LTL = gsl_matrix_alloc(p, p); /* L^T L */ in test_reg4() local 308 gsl_blas_dgemm(CblasTrans, CblasNoTrans, 1.0, L, L, 0.0, LTL); in test_reg4() 309 gsl_matrix_scale(LTL, lambda * lambda); in test_reg4() 312 gsl_matrix_add(XTX, LTL); in test_reg4() 347 gsl_matrix_free(LTL); in test_reg4() 478 gsl_matrix *LTL = gsl_matrix_alloc(p, p); /* Sobolov L^T L */ in test_reg_sobolev() local 494 gsl_blas_dgemm(CblasTrans, CblasNoTrans, 1.0, L, L, 0.0, LTL); in test_reg_sobolev() 518 double aij = gsl_matrix_get(LTL, i, j); in test_reg_sobolev() 530 gsl_matrix_free(LTL); in test_reg_sobolev()
|
/dports/math/spot/spot-2.10.2/doc/ |
H A D | spot.bib | 6 title = {{LTL} to {B\"u}chi Automata Translation: Fast and More 24 Improvements to {LTL} Translation}, 73 title = {{LTL} Model Checking of Interval Markov Chains}, 86 title = {Multi-core SCC-Based LTL Model Checking}, 288 title = {{LTL} Translation Improvements in {Spot}}, 298 focuses on the module translating LTL formul{\ae} into 308 title = {{LTL} Translation Improvements in {S}pot 1.0}, 383 stutter-invariant {LTL}}, 428 title = {Fast {LTL} to {B\"u}chi Automata Translation}, 800 title = {LTL Satisfiability Checking}, [all …]
|
/dports/math/py-spot/spot-2.10.2/doc/ |
H A D | spot.bib | 6 title = {{LTL} to {B\"u}chi Automata Translation: Fast and More 24 Improvements to {LTL} Translation}, 73 title = {{LTL} Model Checking of Interval Markov Chains}, 86 title = {Multi-core SCC-Based LTL Model Checking}, 288 title = {{LTL} Translation Improvements in {Spot}}, 298 focuses on the module translating LTL formul{\ae} into 308 title = {{LTL} Translation Improvements in {S}pot 1.0}, 383 stutter-invariant {LTL}}, 428 title = {Fast {LTL} to {B\"u}chi Automata Translation}, 800 title = {LTL Satisfiability Checking}, [all …]
|
/dports/math/spot/spot-2.10.2/bench/ltlcounter/ |
H A D | README | 1 In the following paper by Rozier & Vardi, a class of LTL formula 6 title = {LTL Satisfiability Checking},
|
/dports/math/py-spot/spot-2.10.2/bench/ltlcounter/ |
H A D | README | 1 In the following paper by Rozier & Vardi, a class of LTL formula 6 title = {LTL Satisfiability Checking},
|
/dports/math/spot/spot-2.10.2/bin/ |
H A D | randltl.cc | 147 spot::randltlgenerator::LTL; 171 output = spot::randltlgenerator::LTL; in parse_opt() 281 case spot::randltlgenerator::LTL: in main()
|
/dports/math/py-spot/spot-2.10.2/bin/ |
H A D | randltl.cc | 147 spot::randltlgenerator::LTL; 171 output = spot::randltlgenerator::LTL; in parse_opt() 281 case spot::randltlgenerator::LTL: in main()
|