diff --git a/src/hoaparse/public.hh b/src/hoaparse/public.hh index 2a7a92922..dc93973bb 100644 --- a/src/hoaparse/public.hh +++ b/src/hoaparse/public.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -34,10 +34,15 @@ namespace spot /// \addtogroup tgba_io /// @{ +#ifndef SWIG /// \brief A parse diagnostic with its location. typedef std::pair hoa_parse_error; /// \brief A list of parser diagnostics, as filled by parse. typedef std::list hoa_parse_error_list; +#else + // Turn hoa_parse_error_list into an opaque type for Swig. + struct hoa_parse_error_list {}; +#endif /// \brief Temporary encoding of an omega automaton produced by /// ltl2hoa. diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index db493aace..ca64c379f 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -544,13 +544,13 @@ elif translator == 'ta': automaton = spot.ensure_digraph(spot.ltl_to_taa(f, dict, refined_rules)) elif translator == 'l3': - l3out = '-T' + l3out = '-H2' # 1.0.1 had determinization and simulation turned off by default, # we need -M0 and -S0 with 1.1.1 for the same effect l3opt = { '-l', '-P', '-A', '-c', '-C', '-o', '-p', '-M0', '-S0' } for lo in form.getfirst('lo', 'T'): if lo == 'U': - l3out = '-T3' # was -U in ltl3ba 1.0.1, now -T3 since 1.1.0 + l3out = '-H3' issba = True for l3 in form.getlist('l3'): if l3 == 'l': @@ -577,26 +577,26 @@ elif translator == 'l3': args.extend(['-f', spot.to_spin_string(f)]) import subprocess l3file = tmpdir + "/aut" - l3aut = open(l3file, "w+") - try: - l3proc = subprocess.Popen(args, stdout=l3aut) - ret = l3proc.wait() - except: - unbufprint('
Failed to run ltl3ba. Is it installed?
') - finish() - if ret != 0: - unbufprint('
ltl3ba exited with error %s
' % ret) - finish() - l3aut.close() - tpel = spot.empty_tgba_parse_error_list() - automaton = spot.tgba_parse(l3file, tpel, dict, env) + with open(l3file, "w+") as l3aut: + try: + l3proc = subprocess.Popen(args, stdout=l3aut) + ret = l3proc.wait() + except: + unbufprint('
Failed to run ltl3ba. Is it installed?
') + finish() + if ret != 0: + unbufprint('
ltl3ba exited with error %s
' % ret) + finish() + tpel = spot.empty_hoa_parse_error_list() + automaton = spot.hoa_parse(l3file, tpel, dict, env) if tpel: unbufprint('''
failed to read ltl3ba's output
''') unbufprint('
') - err = spot.format_tgba_parse_errors(spot.get_cout(), "output", tpel) + err = spot.format_hoa_parse_errors(spot.get_cout(), "output", tpel) unbufprint('
') automaton = 0 finish() + automaton = automaton.aut elif translator == 'cs': donot_inject = False cs_nowdba = True diff --git a/wrap/python/spot.i b/wrap/python/spot.i index b7860451e..a39c6805a 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -33,33 +33,33 @@ %include "std_list.i" %include "exception.i" - // git grep 'typedef.*std::shared_ptr' | grep -v const - // sed 's/.*<\(.*\)>.*/%shared_ptr(spot::\1)/g' -%shared_ptr(spot::bdd_dict) + // git grep 'typedef.*std::shared_ptr' | grep -v const | + // sed 's/.*<\(.*\)>.*/%shared_ptr(spot::\1)/g' %shared_ptr(spot::dstar_aut) -%shared_ptr(spot::future_conditions_collector) +%shared_ptr(spot::hoa_aut) +%shared_ptr(spot::fair_kripke) +%shared_ptr(spot::kripke) +%shared_ptr(spot::kripke_explicit) %shared_ptr(spot::kripke) -%shared_ptr(spot::saba) -%shared_ptr(spot::saba_complement_tgba) %shared_ptr(spot::ta) -%shared_ptr(spot::taa_tgba_formula) -%shared_ptr(spot::taa_tgba_string) %shared_ptr(spot::ta_explicit) %shared_ptr(spot::ta_product) -%shared_ptr(spot::taa_tgba) -%shared_ptr(spot::tgba) -%shared_ptr(spot::tgba_digraph) -%shared_ptr(spot::tgba_kv_complement) -%shared_ptr(spot::tgba_product) -%shared_ptr(spot::tgba_product_init) -%shared_ptr(spot::tgba_safra_complement) -%shared_ptr(spot::tgba_sgba_proxy) %shared_ptr(spot::tgta) %shared_ptr(spot::tgta_explicit) +%shared_ptr(spot::bdd_dict) +%shared_ptr(spot::tgba) +%shared_ptr(spot::tgba_digraph) +%shared_ptr(spot::tgba_product) +%shared_ptr(spot::tgba_product_init) +%shared_ptr(spot::taa_tgba) +%shared_ptr(spot::taa_tgba_string) +%shared_ptr(spot::taa_tgba_formula) +%shared_ptr(spot::tgba_safra_complement) %shared_ptr(spot::tgba_run) -%shared_ptr(spot::emptiness_check) %shared_ptr(spot::emptiness_check_result) +%shared_ptr(spot::emptiness_check) %shared_ptr(spot::emptiness_check_instantiator) +%shared_ptr(spot::tgbasl) namespace std { %template(liststr) list; @@ -131,7 +131,7 @@ namespace std { #include "tgbaalgos/postproc.hh" #include "tgbaalgos/stutter.hh" -#include "tgbaparse/public.hh" +#include "hoaparse/public.hh" #include "ta/ta.hh" #include "ta/tgta.hh" @@ -262,7 +262,7 @@ namespace spot { %include "tgbaalgos/postproc.hh" %include "tgbaalgos/stutter.hh" -%include "tgbaparse/public.hh" +%include "hoaparse/public.hh" %include "ta/ta.hh" %include "ta/tgta.hh" @@ -349,10 +349,10 @@ empty_parse_error_list() return l; } -spot::tgba_parse_error_list -empty_tgba_parse_error_list() +spot::hoa_parse_error_list +empty_hoa_parse_error_list() { - tgba_parse_error_list l; + hoa_parse_error_list l; return l; } @@ -422,7 +422,7 @@ __bool__() } -%extend spot::tgba_parse_error_list { +%extend spot::hoa_parse_error_list { bool __nonzero__() diff --git a/wrap/python/tests/parsetgba.py b/wrap/python/tests/parsetgba.py index c593f9fd4..1431931ce 100755 --- a/wrap/python/tests/parsetgba.py +++ b/wrap/python/tests/parsetgba.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement +# Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -21,24 +21,23 @@ import os import spot contents = ''' -acc = "b"; -"a U b", "1", "b", "b"; -"a U b", "a U b", "a & !b",; -"1", "1", "1", "b"; +HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi +Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc +deterministic --BODY-- State: 0 {0} [t] 0 State: 1 [1] 0 [0&!1] 1 --END-- ''' -filename = 'parsetgba.out' +filename = 'parsetgba.hoa' out = open(filename, 'w+') out.write(contents) out.close() -p = spot.empty_tgba_parse_error_list() -a = spot.tgba_parse(filename, p, spot.make_bdd_dict()) +p = spot.empty_hoa_parse_error_list() +a = spot.hoa_parse(filename, p, spot.make_bdd_dict()) assert not p -spot.dotty_reachable(spot.get_cout(), a) +spot.dotty_reachable(spot.get_cout(), a.aut) del p del a