alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

python: use hoa_parse instead of tgba_parse

Browse source 
* src/hoaparse/public.hh: Cope with SWIG.
* wrap/python/spot.i: Bind hoa_parse instead of tgba_parse.
Remove the binding for tgba_parse because it will be removed
soon from Spot (cf. #1).
* wrap/python/ajax/spot.in: Use the HOA output of ltl3ba.
* wrap/python/tests/parsetgba.py: Adjust test case.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-27 22:44:01 +01:00
parent 6819cee682
commit 44f98219d3
4 changed files with 53 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/hoaparse/public.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -34,10 +34,15 @@ namespace spot
/// \addtogroup tgba_io /// \addtogroup tgba_io
/// @{ /// @{
#ifndef SWIG
/// \brief A parse diagnostic with its location. /// \brief A parse diagnostic with its location.
typedef std::pair<spot::location, std::string> hoa_parse_error; typedef std::pair<spot::location, std::string> hoa_parse_error;
/// \brief A list of parser diagnostics, as filled by parse. /// \brief A list of parser diagnostics, as filled by parse.
typedef std::list<hoa_parse_error> hoa_parse_error_list; typedef std::list<hoa_parse_error> 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 /// \brief Temporary encoding of an omega automaton produced by
/// ltl2hoa. /// ltl2hoa.

14
wrap/python/ajax/spot.in
View file

@ -544,13 +544,13 @@ elif translator == 'ta':
automaton = spot.ensure_digraph(spot.ltl_to_taa(f, dict, refined_rules)) automaton = spot.ensure_digraph(spot.ltl_to_taa(f, dict, refined_rules))
elif translator == 'l3': elif translator == 'l3':
l3out = '-T' l3out = '-H2'
# 1.0.1 had determinization and simulation turned off by default, # 1.0.1 had determinization and simulation turned off by default,
# we need -M0 and -S0 with 1.1.1 for the same effect # we need -M0 and -S0 with 1.1.1 for the same effect
l3opt = { '-l', '-P', '-A', '-c', '-C', '-o', '-p', '-M0', '-S0' } l3opt = { '-l', '-P', '-A', '-c', '-C', '-o', '-p', '-M0', '-S0' }
for lo in form.getfirst('lo', 'T'): for lo in form.getfirst('lo', 'T'):
if lo == 'U': if lo == 'U':
l3out = '-T3' # was -U in ltl3ba 1.0.1, now -T3 since 1.1.0 l3out = '-H3'
issba = True issba = True
for l3 in form.getlist('l3'): for l3 in form.getlist('l3'):
if l3 == 'l': if l3 == 'l':
@ -577,7 +577,7 @@ elif translator == 'l3':
args.extend(['-f', spot.to_spin_string(f)]) args.extend(['-f', spot.to_spin_string(f)])
import subprocess import subprocess
l3file = tmpdir + "/aut" l3file = tmpdir + "/aut"
l3aut = open(l3file, "w+") with open(l3file, "w+") as l3aut:
try: try:
l3proc = subprocess.Popen(args, stdout=l3aut) l3proc = subprocess.Popen(args, stdout=l3aut)
ret = l3proc.wait() ret = l3proc.wait()
@ -587,16 +587,16 @@ elif translator == 'l3':
if ret != 0: if ret != 0:
unbufprint('<div class="error">ltl3ba exited with error %s</div>' % ret) unbufprint('<div class="error">ltl3ba exited with error %s</div>' % ret)
finish() finish()
l3aut.close() tpel = spot.empty_hoa_parse_error_list()
tpel = spot.empty_tgba_parse_error_list() automaton = spot.hoa_parse(l3file, tpel, dict, env)
automaton = spot.tgba_parse(l3file, tpel, dict, env)
if tpel: if tpel:
unbufprint('''<div class="error">failed to read ltl3ba's output</div>''') unbufprint('''<div class="error">failed to read ltl3ba's output</div>''')
unbufprint('<div class="parse-error">') unbufprint('<div class="parse-error">')
err = spot.format_tgba_parse_errors(spot.get_cout(), "output", tpel) err = spot.format_hoa_parse_errors(spot.get_cout(), "output", tpel)
unbufprint('</div>') unbufprint('</div>')
automaton = 0 automaton = 0
finish() finish()
automaton = automaton.aut
elif translator == 'cs': elif translator == 'cs':
donot_inject = False donot_inject = False
cs_nowdba = True cs_nowdba = True

44
wrap/python/spot.i
View file

@ -33,33 +33,33 @@
%include "std_list.i" %include "std_list.i"
%include "exception.i" %include "exception.i"
// git grep 'typedef.*std::shared_ptr' | grep -v const // git grep 'typedef.*std::shared_ptr' | grep -v const |
// sed 's/.*<\(.*\)>.*/%shared_ptr(spot::\1)/g' // sed 's/.*<\(.*\)>.*/%shared_ptr(spot::\1)/g'
%shared_ptr(spot::bdd_dict)
%shared_ptr(spot::dstar_aut) %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::kripke)
%shared_ptr(spot::saba)
%shared_ptr(spot::saba_complement_tgba)
%shared_ptr(spot::ta) %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_explicit)
%shared_ptr(spot::ta_product) %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)
%shared_ptr(spot::tgta_explicit) %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::tgba_run)
%shared_ptr(spot::emptiness_check)
%shared_ptr(spot::emptiness_check_result) %shared_ptr(spot::emptiness_check_result)
%shared_ptr(spot::emptiness_check)
%shared_ptr(spot::emptiness_check_instantiator) %shared_ptr(spot::emptiness_check_instantiator)
%shared_ptr(spot::tgbasl)
namespace std { namespace std {
%template(liststr) list<string>; %template(liststr) list<string>;
@ -131,7 +131,7 @@ namespace std {
#include "tgbaalgos/postproc.hh" #include "tgbaalgos/postproc.hh"
#include "tgbaalgos/stutter.hh" #include "tgbaalgos/stutter.hh"
#include "tgbaparse/public.hh" #include "hoaparse/public.hh"
#include "ta/ta.hh" #include "ta/ta.hh"
#include "ta/tgta.hh" #include "ta/tgta.hh"
@ -262,7 +262,7 @@ namespace spot {
%include "tgbaalgos/postproc.hh" %include "tgbaalgos/postproc.hh"
%include "tgbaalgos/stutter.hh" %include "tgbaalgos/stutter.hh"
%include "tgbaparse/public.hh" %include "hoaparse/public.hh"
%include "ta/ta.hh" %include "ta/ta.hh"
%include "ta/tgta.hh" %include "ta/tgta.hh"
@ -349,10 +349,10 @@ empty_parse_error_list()
return l; return l;
} }
spot::tgba_parse_error_list spot::hoa_parse_error_list
empty_tgba_parse_error_list() empty_hoa_parse_error_list()
{ {
tgba_parse_error_list l; hoa_parse_error_list l;
return l; return l;
} }
@ -422,7 +422,7 @@ __bool__()
} }
%extend spot::tgba_parse_error_list { %extend spot::hoa_parse_error_list {
bool bool
__nonzero__() __nonzero__()

17
wrap/python/tests/parsetgba.py
View file

@ -1,5 +1,5 @@
# -*- mode: python; coding: utf-8 -*- # -*- 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). # de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -21,24 +21,23 @@ import os
import spot import spot
contents = ''' contents = '''
acc = "b"; HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi
"a U b", "1", "b", "b"; Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc
"a U b", "a U b", "a & !b",; deterministic --BODY-- State: 0 {0} [t] 0 State: 1 [1] 0 [0&!1] 1 --END--
"1", "1", "1", "b";
''' '''
filename = 'parsetgba.out' filename = 'parsetgba.hoa'
out = open(filename, 'w+') out = open(filename, 'w+')
out.write(contents) out.write(contents)
out.close() out.close()
p = spot.empty_tgba_parse_error_list() p = spot.empty_hoa_parse_error_list()
a = spot.tgba_parse(filename, p, spot.make_bdd_dict()) a = spot.hoa_parse(filename, p, spot.make_bdd_dict())
assert not p assert not p
spot.dotty_reachable(spot.get_cout(), a) spot.dotty_reachable(spot.get_cout(), a.aut)
del p del p
del a del a