Issues · Spot / Spot

New issue

Streett changes for HOA 1.1 2 of 6 tasks completed

#249 · opened Mar 26, 2017 by Alexandre Duret-Lutz Spot 2.7 hoa wish
- 2
updated Nov 08, 2018
libspotgen

#254 · opened Apr 20, 2017 by Alexandre Duret-Lutz build wish
- CLOSED
- 2
updated Apr 25, 2017
autfilt --split-edges

#255 · opened Apr 21, 2017 by Alexandre Duret-Lutz wish
- CLOSED
- 0
updated May 09, 2017
fixing the closure operator to better match the PSL standard

#242 · opened Mar 13, 2017 by Alexandre Duret-Lutz spot 2.3.2 bug doc rewritings tl wish
- CLOSED
- 1
updated Apr 28, 2017
copy() -> make_twa_graph()

#258 · opened May 03, 2017 by Alexandre Duret-Lutz Spot 2.4 short task wish
- CLOSED
- 0
updated Jul 25, 2017
translation to improve

#263 · opened May 16, 2017 by Alexandre Duret-Lutz wish
- CLOSED
- 0
updated Sep 02, 2017
translation to improve

#264 · opened May 16, 2017 by Alexandre Duret-Lutz wish
- 0
updated Sep 02, 2017
more families of LTL formulas for genltl

#265 · opened May 17, 2017 by Alexandre Duret-Lutz gen wish
- 0
updated Jun 09, 2017
Transform Alternating Automata into Weak Alternating Automata 3 of 4 tasks completed

#266 · opened Jun 09, 2017 by Thomas Medioni wish
- 0
updated Oct 01, 2017
a formula to optimize

#267 · opened Jun 14, 2017 by Alexandre Duret-Lutz wish
- CLOSED
- 2
updated Jun 29, 2018
Boolean rewriting as a speedup

#268 · opened Jun 19, 2017 by Alexandre Duret-Lutz wish
- CLOSED
- 0
updated Jun 23, 2017
streett-like to streett

#272 · opened Jun 21, 2017 by Alexandre Duret-Lutz short task wish
- 0
updated Jun 21, 2017
sbacc on alternating automata

#273 · opened Jun 28, 2017 by Thomas Medioni wish
- CLOSED
- 0
updated Jul 24, 2017
is_inherently_weak should support alternating automata

#275 · opened Jul 20, 2017 by Thomas Medioni wish
- 1
updated Aug 09, 2017
missed simplifications

#173 · opened May 04, 2016 by Alexandre Duret-Lutz bug simulation wish
- 1
updated Sep 06, 2017
SPOT_PARSE_LOCATION

#232 · opened Feb 19, 2017 by Alexandre Duret-Lutz wish
- 1
updated Sep 06, 2017
Add other logics to Spot 0 of 4 tasks completed

#225 · opened Feb 10, 2017 by Maximilien Colange wish
- 1
updated Sep 06, 2017
autfilt --when EXPR

#222 · opened Feb 04, 2017 by Alexandre Duret-Lutz wish
- 0
updated Sep 06, 2017
overhaul the formula simplification routines 0 of 5 tasks completed

#281 · opened Sep 15, 2017 by Alexandre Duret-Lutz tl wish
- 0
updated Sep 15, 2017
ltldo -n

#287 · opened Oct 02, 2017 by Alexandre Duret-Lutz short task wish
- CLOSED
- 0
updated Oct 05, 2017
autfilt --acceptance-is=...

#288 · opened Oct 02, 2017 by Alexandre Duret-Lutz short task wish
- CLOSED
- 0
updated Nov 04, 2017
autfilt --stats=%[n]g

#289 · opened Oct 02, 2017 by Alexandre Duret-Lutz short task wish
- CLOSED
- 0
updated Nov 04, 2017
ltl2tgba --parity and autfilt --parity

#290 · opened Oct 02, 2017 by Alexandre Duret-Lutz wish
- CLOSED
- 2
updated Feb 16, 2018
ltlcross --reference

#295 · opened Oct 11, 2017 by Alexandre Duret-Lutz wish
- CLOSED
- 0
updated Oct 15, 2017
trivial acceptance simplifications missing

#297 · opened Nov 06, 2017 by Alexandre Duret-Lutz short task wish
- CLOSED
- 1
updated Nov 06, 2017
connect tgba_determinize() and dtwa_sat_minimize() in ltl2tgba

#177 · opened May 17, 2016 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
option to limit stack depth in emptiness checks

#209 · opened Jan 27, 2017 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
more colors

#202 · opened Jan 04, 2017 by Alexandre Duret-Lutz short task wish
- CLOSED
- 1
updated Jan 05, 2018
ltlcross -D should allow setting a limit to the size of the deterministic automaton

#169 · opened Apr 27, 2016 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
macport

#201 · opened Dec 14, 2016 by Etienne Renault darwin wish
- 0
updated Nov 15, 2017
Tell valgrind about memory pools

#200 · opened Dec 05, 2016 by Maximilien Colange wish
- CLOSED
- 1
updated Jun 20, 2018
Rewrite testing automata as Fin( ! 0)

#163 · opened Apr 25, 2016 by Etienne Renault wish
- 0
updated Nov 15, 2017
Produce fair Kripke when loading DVE file

#151 · opened Feb 15, 2016 by Etienne Renault wish
- 0
updated Nov 15, 2017
case where ltlcross consumes too much memory

#140 · opened Feb 05, 2016 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
improve detection and handling of weak automata in remove_fin()

#183 · opened Jul 13, 2016 by Alexandre Duret-Lutz wish
- 1
updated Nov 15, 2017
add an intersect() method to twa_graph

#127 · opened Dec 09, 2015 by Alexandre Duret-Lutz wish
- 1
updated Jun 28, 2018
implement simulation-based inclusion checks

#182 · opened Jun 28, 2016 by Alexandre Duret-Lutz simulation wish
- 0
updated Nov 15, 2017
Python API documentation

#124 · opened Nov 17, 2015 by Alexandre Duret-Lutz wish
- 1
updated Nov 15, 2017
missed simplification

#180 · opened Jun 13, 2016 by Alexandre Duret-Lutz simulation wish
- 0
updated Nov 15, 2017
minimize_wdba() should have improved detection of terminal automata in its output

#121 · opened Nov 06, 2015 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
minimize_wdba() should be specialized for terminal automata

#120 · opened Nov 06, 2015 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
Automatic build for various distributions

#111 · opened Oct 09, 2015 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
named temporal operators

#102 · opened Aug 14, 2015 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
An example of BA translation that is better than its original TGBA

#75 · opened Apr 16, 2015 by Alexandre Duret-Lutz wish
- 2
updated Dec 14, 2020
'Step by step' mode for algorithms in python

#74 · opened Apr 09, 2015 by Etienne Renault wish
- 0
updated Nov 15, 2017
are_isomorphic and canonicalize should also consider reorderings of acceptance sets

#58 · opened Feb 20, 2015 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
hoa: use acc-name to validate Acceptance

#54 · opened Jan 28, 2015 by Alexandre Duret-Lutz hoa wish
- 0
updated Nov 15, 2017
fusion-star support 4 of 7 tasks completed

#51 · opened Jan 15, 2015 by Alexandre Duret-Lutz wish
- 1
updated Nov 15, 2017
improve failure reporting of ltlcross

#38 · opened Dec 19, 2014 by Alexandre Duret-Lutz wish
- 1
updated Nov 15, 2017
implement a feed-back arc set heuristic

#37 · opened Dec 19, 2014 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
PSL and persistent formulas

#29 · opened Dec 19, 2014 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
Finalize PSL support 0 of 4 tasks completed

#28 · opened Dec 19, 2014 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
improve syntactic characterization to take simplification rules into account

#10 · opened Dec 19, 2014 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
improve remove-x

#27 · opened Dec 19, 2014 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
simplify {r;1} as {r}

#3 · opened Dec 06, 2014 by Alexandre Duret-Lutz rewritings short task wish
- CLOSED
- 1
updated May 07, 2018
find a way to reduce {b*;r} = (b W r) when r is satisfiable

#2 · opened Dec 06, 2014 by Alexandre Duret-Lutz rewritings wish
- 0
updated Nov 15, 2017
improve speed of wdba-minimization

#26 · opened Dec 19, 2014 by Alexandre Duret-Lutz wish
- 3
updated Nov 15, 2017
ltlfilt --ltl=subclass

#24 · opened Dec 19, 2014 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
rewrite the web page ltl2tgba.html so its interface is similar to that of the command-line ltl2tgba

#18 · opened Dec 19, 2014 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
add an option to do WDBA-minimization only when we are sure it will succeed

#15 · opened Dec 19, 2014 by Alexandre Duret-Lutz wish
- CLOSED
- 0
updated Jul 13, 2020
better compilation options

#13 · opened Dec 19, 2014 by Alexandre Duret-Lutz wish
- 0
updated Nov 15, 2017
even more LTL simplification for GF formulas

#12 · opened Dec 19, 2014 by Alexandre Duret-Lutz rewritings wish
- 0
updated Nov 15, 2017
allow unabbreviation before converting formulas in ltldo and ltlcross

#168 · opened Apr 27, 2016 by Alexandre Duret-Lutz bug wish
- CLOSED
- 0
updated Nov 15, 2017
rewrite minimize_dfa using the twa_graph interface

#233 · opened Feb 22, 2017 by Alexandre Duret-Lutz Spot 2.4 wish
- CLOSED
- 0
updated Dec 02, 2020
co-Büching Them All

#219 · opened Feb 02, 2017 by Alexandre Gbaguidi Aïsse wish
- CLOSED
- 1
updated Nov 15, 2017
a simple acceptance set simplification

#216 · opened Feb 01, 2017 by Alexandre Duret-Lutz wish
- CLOSED
- 1
updated Nov 15, 2017
automata-subclasses naming mess

#212 · opened Jan 31, 2017 by Alexandre Duret-Lutz Spot 2.4 hoa wish
- CLOSED
- 2
updated Nov 15, 2017
ltldo --smallest / ltldo --largest

#206 · opened Jan 23, 2017 by Alexandre Duret-Lutz Spot 2.3.1 idea wish
- CLOSED
- 0
updated Nov 15, 2017
less "costly" coloring scheme from highlight_languages()

#203 · opened Jan 05, 2017 by Alexandre Duret-Lutz short task wish
- CLOSED
- 0
updated Nov 15, 2017
improve data storage in SAT-minimization

#191 · opened Oct 25, 2016 by Alexandre Duret-Lutz wish
- CLOSED
- 2
updated Nov 15, 2017
optimize is_unambiguous for Streett automata

#188 · opened Oct 17, 2016 by Alexandre Duret-Lutz wish
- CLOSED
- 3
updated Nov 15, 2017
assert in headers 4 of 4 tasks completed

#184 · opened Jul 20, 2016 by Alexandre Duret-Lutz wish
- CLOSED
- 3
updated Nov 15, 2017
confusing range diagnostic

#181 · opened Jun 21, 2016 by Alexandre Duret-Lutz short task wish
- CLOSED
- 0
updated Nov 15, 2017
convertion to generalized Rabin

#174 · opened May 09, 2016 by Alexandre Duret-Lutz wish
- CLOSED
- 0
updated Nov 15, 2017
genltl should have options to generate the formula from bench/ltl2tgba/formulae.ltl

#166 · opened Apr 27, 2016 by Alexandre Duret-Lutz wish
- CLOSED
- 0
updated Nov 15, 2017
is_deterministic, is_weak, etc should set the property

#165 · opened Apr 27, 2016 by Alexandre Duret-Lutz short task wish
- CLOSED
- 0
updated Nov 15, 2017
`autfilt --check=stutter` should work for non-deterministic automata

#164 · opened Apr 27, 2016 by Alexandre Duret-Lutz short task wish
- CLOSED
- 0
updated Nov 15, 2017
add support for %%promela

#162 · opened Apr 22, 2016 by Etienne Renault wish
- CLOSED
- 0
updated Nov 15, 2017
Coding style: tab and spaces

#156 · opened Mar 08, 2016 by Laurent Xu Spot 2.0 wish
- CLOSED
- 2
updated Nov 15, 2017
rename or get rid spot::tgba_reachable_iterator

#155 · opened Mar 03, 2016 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 1
updated Nov 15, 2017
aut.is_empty() does not return a counterexample

#153 · opened Feb 16, 2016 by Etienne Renault wish
- CLOSED
- 1
updated Nov 15, 2017
get rid of twa::transition_annotation() ?

#149 · opened Feb 15, 2016 by Alexandre Duret-Lutz Spot 2.0 short task wish
- CLOSED
- 0
updated Nov 15, 2017
get rid of twa::support_conditions()

#148 · opened Feb 14, 2016 by Alexandre Duret-Lutz Spot 2.0 short task wish
- CLOSED
- 0
updated Nov 15, 2017
Improve speed of product_n

#139 · opened Feb 03, 2016 by Laurent Xu wish
- CLOSED
- 1
updated Nov 15, 2017
print_dot should support option "k" as in print_hoa

#134 · opened Jan 31, 2016 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 0
updated Nov 15, 2017
twa::~twa should call unregister_all_my_variables()

#129 · opened Jan 07, 2016 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 0
updated Nov 15, 2017
add option to highlight non-determinism in dot output

#123 · opened Nov 13, 2015 by Alexandre Duret-Lutz short task wish
- CLOSED
- 1
updated Nov 15, 2017
"property: weak" should imply prop_inherently_weak

#119 · opened Nov 05, 2015 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 0
updated Nov 15, 2017
show more properties in tut21, and add a Python version

#118 · opened Nov 04, 2015 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 0
updated Nov 15, 2017
add Python binding for spot::is_unambiguous()

#117 · opened Nov 04, 2015 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 0
updated Nov 15, 2017
twa::is_deterministic(), twa::is_unambiguous() and friends are confusing

#116 · opened Nov 04, 2015 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 0
updated Nov 15, 2017
add a trust option to the parser

#114 · opened Oct 22, 2015 by Alexandre Duret-Lutz wish
- CLOSED
- 0
updated Nov 15, 2017
improve bindings for counterexample output

#113 · opened Oct 16, 2015 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 0
updated Nov 15, 2017
compile with -Wzero-as-null-pointer-constant

#106 · opened Sep 24, 2015 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 0
updated Nov 15, 2017
add an option to autfilt to match automata that recognize a given word

#109 · opened Sep 30, 2015 by Alexandre Duret-Lutz wish
- CLOSED
- 0
updated Nov 15, 2017
--unabbreviate=R

#103 · opened Aug 20, 2015 by Alexandre Duret-Lutz Spot 2.0 short task wish
- CLOSED
- 0
updated Nov 15, 2017
web site should display notebook examples

#100 · opened Jul 24, 2015 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 0
updated Nov 15, 2017
ltlgrind should have -f or -F by default

#107 · opened Sep 24, 2015 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 0
updated Nov 15, 2017
speed up exec() in ltlcross and ltldo

#98 · opened Jul 16, 2015 by Alexandre Duret-Lutz wish
- CLOSED
- 0
updated Nov 15, 2017
diagnose missing Python.h in configure

#95 · opened Jun 29, 2015 by Alexandre Duret-Lutz Spot 2.0 wish
- CLOSED
- 0
updated Nov 15, 2017