
hi there, smth is wrong with online translator for LTL3BA -- see message below. Thanks for amazing web-page! regards, ayrat *RuntimeError* Python 3.4.2: /usr/bin/python3 Thu Jul 7 11:57:15 2016 A problem occurred in a Python script. Here is the sequence of function calls leading up to the error, in the order they occurred. /var/www/html/cgi-bin/spotcgi.py <file:///var/www/html/cgi-bin/spotcgi.py> in **() 747 dont_run_dot = print_stats(degen, True) 748 automaton.set_name(str(f)) => 749 render_automaton(degen, dont_run_dot) 750 degen = 0 751 automaton = 0 *render_automaton* = <function render_automaton>, *degen* = <spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >, *dont_run_dot* = False /var/www/html/cgi-bin/spotcgi.py <file:///var/www/html/cgi-bin/spotcgi.py> in *render_automaton*(automaton=<spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >, dont_run_dot=False) 314 else: # TGBA 315 if not dont_run_dot: => 316 hoaname = save_hoa(automaton) 317 spot.print_dot(dotsrc, automaton, '.t' if buchi_type == 't' else '.') 318 render_dot_maybe(dotsrc.str(), dont_run_dot, hoaname) *hoaname* = None, /global/ *save_hoa* = <function save_hoa>, *automaton* = <spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> > /var/www/html/cgi-bin/spotcgi.py <file:///var/www/html/cgi-bin/spotcgi.py> in *save_hoa*(automaton=<spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >) 259 def save_hoa(automaton): 260 hoasrc = spot.ostringstream() => 261 spot.print_hoa(hoasrc, automaton, 't' if buchi_type == 't' else '') 262 hoasrc = hoasrc.str() 263 hoasrc += '\n' /global/ *spot* = <module 'spot' from '/usr/lib/python3/dist-packages/spot/__init__.py'>, spot.*print_hoa* = <built-in function print_hoa>, *hoasrc* = <spot.impl.ostringstream; proxy of <Swig Object of type 'std::ostringstream *' at 0x7f2ae4164d20>
, *automaton* = <spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >, /global/ *buchi_type* = 't'
*RuntimeError*: print_hoa(): automaton uses unregistered atomic propositions args = ('print_hoa(): automaton uses unregistered atomic propositions',) with_traceback = <built-in method with_traceback of RuntimeError object>

On Thu, Jul 7, 2016 at 1:59 PM, Ayrat <ayrat.khalimov@iaik.tugraz.at> wrote:
hi there,
smth is wrong with online translator for LTL3BA -- see message below. Thanks for amazing web-page!
Dear Ayat, Thank you for the report. Do you remember what formula you translated? (I tried a few formulas without being able to reproduce the error.)

yes, sorry, just realized that it works for other formulas: here is the formula: link: https://spot.lrde.epita.fr/trans.html#f=((F+(b+%26%26+G+F+a)+%7C%7C+F(c+%26%26+G+F+!a))+%26%26+F+b+%26%26+F+c)+%3C-%3E+GF+p0&r=br&r=lf&r=si&r=eu&o=a&ff=o&mf=n&af=t&ra=t&rf=d&tf=a&t=l3&fm=od&fm=sm&ta=lc&lo=U&l3=l&l3=A&l3=P&l3=o&l3=p&l3=C&l3=M&l3=S&cs=s&as=ps&as=wd&ec=Cou99&eo=&to=m formula: ((F (b && G F a) || F(c && G F !a)) && F b && F c) <-> GF p0 regards, ayrat On Thu, Jul 7, 2016 at 5:13 PM, Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
On Thu, Jul 7, 2016 at 1:59 PM, Ayrat <ayrat.khalimov@iaik.tugraz.at> wrote:
hi there,
smth is wrong with online translator for LTL3BA -- see message below. Thanks for amazing web-page!
Dear Ayat,
Thank you for the report. Do you remember what formula you translated? (I tried a few formulas without being able to reproduce the error.)
_______________________________________________ Spot mailing list Spot@lrde.epita.fr https://lists.lrde.epita.fr/listinfo/spot
participants (3)
-
Alexandre Duret-Lutz
-
Ayrat
-
Ayrat Khalimov