c2ae99e779
Now that we support any type of omega-accetpance, not just "Generalized Büchi", it is time to move away from GB and replace it by "ω", written just w in ASCII. This just change the name of the tgba class. This part has to be done by hand because the word "tgba" occurs in many contexts and a mass replacement would be wrong. This will be followed by some automatic renaming of all the derived types and more. * src/bin/autfilt.cc, src/bin/randaut.cc, src/kripke/fairkripke.hh, src/ta/tgta.cc, src/ta/tgta.hh, src/tgba/fwd.hh, src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc, src/tgba/tgba.hh, src/tgba/tgbagraph.hh, src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh, src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh, src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/cleanacc.cc, src/tgbaalgos/dotty.cc, src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh, src/tgbaalgos/hoa.cc, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/simulation.cc, src/tgbaalgos/stutter.cc, src/tgbatest/checkpsl.cc, src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc, wrap/python/spot.py, wrap/python/spot_impl.i: Rename the tgba class into twa.
441 lines
16 KiB
Python
441 lines
16 KiB
Python
# -*- coding: utf-8 -*-
|
|
# Copyright (C) 2014, 2015 Laboratoire de
|
|
# Recherche et Développement de l'Epita (LRDE).
|
|
#
|
|
# This file is part of Spot, a model checking library.
|
|
#
|
|
# Spot is free software; you can redistribute it and/or modify it
|
|
# under the terms of the GNU General Public License as published by
|
|
# the Free Software Foundation; either version 3 of the License, or
|
|
# (at your option) any later version.
|
|
#
|
|
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
|
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
|
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
|
# License for more details.
|
|
#
|
|
# You should have received a copy of the GNU General Public License
|
|
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
|
|
|
from spot_impl import *
|
|
import subprocess
|
|
import sys
|
|
from functools import lru_cache
|
|
|
|
# Global BDD dict so that we do not have to create one in user code.
|
|
_bdd_dict = make_bdd_dict()
|
|
|
|
# Load all preliminaries for a fancy display
|
|
def setup(show_bullet=True):
|
|
import os
|
|
os.environ['SPOT_DOTEXTRA'] = 'size="10.2,5" node[style=filled,fillcolor="#ffffaa"] edge[arrowhead=vee, arrowsize=.7]'
|
|
if show_bullet:
|
|
os.environ['SPOT_DOTDEFAULT'] = 'rbcf(Lato)'
|
|
else:
|
|
os.environ['SPOT_DOTDEFAULT'] = 'rcf(Lato)'
|
|
|
|
# Add a small LRU cache so that when we display automata into a
|
|
# interactive widget, we avoid some repeated calls to dot for
|
|
# identical inputs.
|
|
@lru_cache(maxsize=64)
|
|
def _str_to_svg(str):
|
|
dotty = subprocess.Popen(['dot', '-Tsvg'],
|
|
stdin=subprocess.PIPE,
|
|
stdout=subprocess.PIPE)
|
|
dotty.stdin.write(str)
|
|
res = dotty.communicate()
|
|
return res[0].decode('utf-8')
|
|
|
|
def _ostream_to_svg(ostr):
|
|
return _str_to_svg(ostr.str().encode('utf-8'))
|
|
|
|
def _render_automaton_as_svg(a, opt=None):
|
|
ostr = ostringstream()
|
|
dotty_reachable(ostr, a, opt)
|
|
return _ostream_to_svg(ostr)
|
|
|
|
twa._repr_svg_ = _render_automaton_as_svg
|
|
ta._repr_svg_ = _render_automaton_as_svg
|
|
|
|
def _render_formula_as_svg(a):
|
|
# Load the SVG function only if we need it. This way the bindings
|
|
# can still be used outside of IPython if IPython is not
|
|
# installed.
|
|
from IPython.display import SVG
|
|
ostr = ostringstream()
|
|
dotty(ostr, a)
|
|
return SVG(_ostream_to_svg(ostr))
|
|
|
|
def _return_automaton_as_svg(a, opt=None):
|
|
# Load the SVG function only if we need it. This way the bindings
|
|
# can still be used outside of IPython if IPython is not
|
|
# installed.
|
|
from IPython.display import SVG
|
|
return SVG(_render_automaton_as_svg(a, opt))
|
|
twa.show = _return_automaton_as_svg
|
|
ta.show = _return_automaton_as_svg
|
|
|
|
def _formula_str_ctor(self, str):
|
|
self.this = parse_formula(str)
|
|
|
|
def _formula_to_str(self, format = 'spot'):
|
|
if format == 'spot':
|
|
return to_string(self)
|
|
elif format == 'spin':
|
|
return to_spin_string(self)
|
|
elif format == 'utf8':
|
|
return to_utf8_string(self)
|
|
elif format == 'lbt':
|
|
return to_lbt_string(self)
|
|
elif format == 'wring':
|
|
return to_wring_string(self)
|
|
elif format == 'latex':
|
|
return to_latex_string(self)
|
|
elif format == 'sclatex':
|
|
return to_sclatex_string(self)
|
|
else:
|
|
raise ValueError("unknown string format: " + format)
|
|
|
|
formula.__init__ = _formula_str_ctor
|
|
formula.to_str = _formula_to_str
|
|
formula.show_ast = _render_formula_as_svg
|
|
|
|
def _twa_to_str(a, format='hoa', opt=None):
|
|
format = format.lower()
|
|
if format == 'hoa':
|
|
ostr = ostringstream()
|
|
hoa_reachable(ostr, a, opt)
|
|
return ostr.str()
|
|
if format == 'dot':
|
|
ostr = ostringstream()
|
|
dotty_reachable(ostr, a, opt)
|
|
return ostr.str()
|
|
if format == 'spin':
|
|
ostr = ostringstream()
|
|
never_claim_reachable(ostr, a, opt)
|
|
return ostr.str()
|
|
if format == 'lbtt':
|
|
ostr = ostringstream()
|
|
lbtt_reachable(ostr, a, bool(opt))
|
|
return ostr.str()
|
|
raise ValueError("unknown string format: " + format)
|
|
|
|
def _twa_save(a, filename, format='hoa', opt=None, append=False):
|
|
with open(filename, 'a' if append else 'w') as f:
|
|
s = a.to_str(format, opt)
|
|
f.write(s)
|
|
if s[-1] != '\n':
|
|
f.write('\n')
|
|
return a
|
|
|
|
twa.to_str = _twa_to_str
|
|
twa.save = _twa_save
|
|
|
|
def automata(*filenames):
|
|
"""Read automata from a list of filenames.
|
|
|
|
The automata can be written in the
|
|
[HOA format](http://adl.github.io/hoaf/), as
|
|
[never claims](http://spinroot.com/spin/Man/never.html),
|
|
or in [LBTT's format]
|
|
(http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html).
|
|
|
|
If a filename ends with a `|`, then the filename is interpreted as
|
|
a shell command, and the output of that command (without the `|`)
|
|
is parsed."""
|
|
|
|
for filename in filenames:
|
|
try:
|
|
p = None
|
|
if filename[-1] != '|':
|
|
proc = None
|
|
p = hoa_stream_parser(filename, True)
|
|
else:
|
|
proc = subprocess.Popen(filename[:-1], shell=True,
|
|
stdout=subprocess.PIPE)
|
|
p = hoa_stream_parser(proc.stdout.fileno(), filename, True)
|
|
a = True
|
|
while a:
|
|
# This returns None when we reach the end of the file.
|
|
a = p.parse_strict(_bdd_dict)
|
|
if a:
|
|
yield a
|
|
finally:
|
|
# Make sure we destroy the parser (p) and the subprocess
|
|
# (prop) in the correct order...
|
|
del p
|
|
if proc != None:
|
|
if not a:
|
|
# We reached the end of the stream. Wait for the
|
|
# process to finish, so that we can its exit code.
|
|
ret = proc.wait()
|
|
else:
|
|
# if a != None, we probably got there through an
|
|
# exception, and the subprocess my still be
|
|
# running. Check if an exit status is available
|
|
# just in case.
|
|
ret = proc.poll()
|
|
del proc
|
|
if ret:
|
|
raise RuntimeError("Command {} exited with exit status {}"
|
|
.format(filename[:-1], ret))
|
|
return
|
|
|
|
def automaton(filename):
|
|
"""Read a single automaton from a file.
|
|
|
|
See `spot.automata()` for a list of supported formats."""
|
|
try:
|
|
return next(automata(filename))
|
|
except StopIteration:
|
|
raise RuntimeError("Failed to read automaton from {}".format(filename))
|
|
|
|
def translate(formula, output='tgba', pref='small', level='high',
|
|
complete=False):
|
|
"""Translate a formula into an automaton.
|
|
|
|
Keep in mind that pref expresses just a preference that may not be
|
|
satisfied.
|
|
|
|
Keyword arguments:
|
|
output -- the type of automaton to build ('tgba', 'ba', 'monitor')
|
|
pref -- prefered characteristic of the produced automaton
|
|
('small', 'deterministic', 'any')
|
|
level -- level of optimizations ('low', 'medium', 'high')
|
|
complete -- whether to produce a complete automaton (True, False)
|
|
"""
|
|
if type(formula) == str:
|
|
formula = parse_formula(formula)
|
|
|
|
a = translator(_bdd_dict)
|
|
|
|
if type(output) == str:
|
|
output_ = output.lower()
|
|
if output_ == 'tgba':
|
|
output = postprocessor.TGBA
|
|
elif output_ == 'ba':
|
|
output = postprocessor.BA
|
|
elif output_.startswith('mon'):
|
|
output = postprocessor.Monitor
|
|
else:
|
|
raise ValueError("unknown output type: " + output)
|
|
a.set_type(output)
|
|
|
|
if complete:
|
|
complete = postprocessor.Complete
|
|
else:
|
|
complete = 0
|
|
|
|
if type(pref) == str:
|
|
pref_ = pref.lower()
|
|
if pref_.startswith('sm'):
|
|
pref = postprocessor.Small
|
|
elif pref_.startswith('det'):
|
|
pref = postprocessor.Deterministic
|
|
elif pref_ == 'any':
|
|
pref = postprocessor.Any
|
|
else:
|
|
raise ValueError("unknown output preference: " + pref)
|
|
a.set_pref(pref | complete)
|
|
|
|
if type(level) == str:
|
|
level_ = level.lower()
|
|
if level_ == 'high':
|
|
level = postprocessor.High
|
|
elif level_.startswith('med'):
|
|
level = postprocessor.Medium
|
|
elif level_ == 'low':
|
|
level = postprocessor.Low
|
|
else:
|
|
raise ValueError("unknown optimization level: " + level)
|
|
a.set_level(level)
|
|
|
|
return a.run(formula)
|
|
|
|
formula.translate = translate
|
|
|
|
# Wrapper around a formula iterator to which we add some methods of formula
|
|
# (using _addfilter and _addmap), so that we can write things like
|
|
# formulas.simplify().is_X_free().
|
|
class formulaiterator:
|
|
def __init__(self, formulas):
|
|
self._formulas = formulas
|
|
|
|
def __iter__(self):
|
|
return self
|
|
|
|
def __next__(self):
|
|
return next(self._formulas)
|
|
|
|
# fun shoud be a predicate and should be a method of formula.
|
|
# _addfilter adds this predicate as a filter whith the same name in
|
|
# formulaiterator.
|
|
def _addfilter(fun):
|
|
def filtf(self, *args, **kwargs):
|
|
it = filter(lambda f: getattr(f, fun)(*args, **kwargs), self)
|
|
return formulaiterator(it)
|
|
def nfiltf(self, *args, **kwargs):
|
|
it = filter(lambda f: not getattr(f, fun)(*args, **kwargs), self)
|
|
return formulaiterator(it)
|
|
setattr(formulaiterator, fun, filtf)
|
|
if fun[:3] == 'is_':
|
|
notfun = fun[:3] + 'not_' + fun[3:]
|
|
elif fun[:4] == 'has_':
|
|
notfun = fun[:4] + 'no_' + fun[4:]
|
|
else:
|
|
notfun = 'not_' + fun
|
|
setattr(formulaiterator, fun, filtf)
|
|
setattr(formulaiterator, notfun, nfiltf)
|
|
|
|
# fun should be a function taking a formula as its first parameter and returning
|
|
# a formula.
|
|
# _addmap adds this function as a method of formula and formulaiterator.
|
|
def _addmap(fun):
|
|
def mapf(self, *args, **kwargs):
|
|
return formulaiterator(map(lambda f: getattr(f, fun)(*args, **kwargs),
|
|
self))
|
|
setattr(formula, fun, lambda self, *args, **kwargs: globals()[fun](self,
|
|
*args, **kwargs))
|
|
setattr(formulaiterator, fun, mapf)
|
|
|
|
def randltl(ap, n = -1, **kwargs):
|
|
"""Generate random formulas.
|
|
|
|
Returns a random formula iterator.
|
|
|
|
ap: the number of atomic propositions used to generate random formulas.
|
|
|
|
n: number of formulas to generate, or unbounded if n < 0.
|
|
|
|
**kwargs:
|
|
seed: seed for the random number generator (0).
|
|
output: can be 'ltl', 'psl', 'bool' or 'sere' ('ltl').
|
|
allow_dups: allow duplicate formulas (False).
|
|
tree_size: tree size of the formulas generated, before mandatory
|
|
simplifications (15)
|
|
boolean_priorities: set priorities for Boolean formulas.
|
|
ltl_priorities: set priorities for LTL formulas.
|
|
sere_priorities: set priorities for SERE formulas.
|
|
dump_priorities: show current priorities, do not generate any formula.
|
|
simplify:
|
|
0 No rewriting
|
|
1 basic rewritings and eventual/universal rules
|
|
2 additional syntactic implication rules
|
|
3 (default) better implications using containment
|
|
"""
|
|
opts = option_map()
|
|
output_map = {
|
|
"ltl" : OUTPUTLTL,
|
|
"psl" : OUTPUTPSL,
|
|
"bool" : OUTPUTBOOL,
|
|
"sere" : OUTPUTSERE
|
|
}
|
|
|
|
if isinstance(ap, list):
|
|
aprops = atomic_prop_set()
|
|
e = default_environment.instance()
|
|
for elt in ap:
|
|
aprops.insert(is_atomic_prop(e.require(elt)))
|
|
ap = aprops
|
|
ltl_priorities = kwargs.get("ltl_priorities", None)
|
|
sere_priorities = kwargs.get("sere_priorities", None)
|
|
boolean_priorities = kwargs.get("boolean_priorities", None)
|
|
output = output_map[kwargs.get("output", "ltl")]
|
|
opts.set("output", output)
|
|
opts.set("seed", kwargs.get("seed", 0))
|
|
tree_size = kwargs.get("tree_size", 15)
|
|
if isinstance(tree_size, tuple):
|
|
tree_size_min, tree_size_max = tree_size
|
|
else:
|
|
tree_size_min = tree_size_max = tree_size
|
|
opts.set("tree_size_min", tree_size_min)
|
|
opts.set("tree_size_max", tree_size_max)
|
|
opts.set("unique", not kwargs.get("allow_dups", False))
|
|
opts.set("wf", kwargs.get("weak_fairness", False))
|
|
simpl_level = kwargs.get("simplify", 0)
|
|
if simpl_level > 3 or simpl_level < 0:
|
|
sys.stderr.write('invalid simplification level: ' + simpl_level)
|
|
return
|
|
opts.set("simplification_level", simpl_level)
|
|
|
|
rg = randltlgenerator(ap, opts, ltl_priorities, sere_priorities,
|
|
boolean_priorities)
|
|
|
|
dump_priorities = kwargs.get("dump_priorities", False)
|
|
if dump_priorities:
|
|
dumpstream = ostringstream()
|
|
if output == OUTPUTLTL:
|
|
print('Use argument ltl_priorities=STRING to set the following ' \
|
|
'LTL priorities:\n')
|
|
rg.dump_ltl_priorities(dumpstream)
|
|
print(dumpstream.str())
|
|
elif output == OUTPUTBOOL:
|
|
print('Use argument boolean_priorities=STRING to set the ' \
|
|
'following Boolean formula priorities:\n')
|
|
rg.dump_bool_priorities(dumpstream)
|
|
print(dumpstream.str())
|
|
elif output == OUTPUTPSL or output == OUTPUTSERE:
|
|
if output != OUTPUTSERE:
|
|
print('Use argument ltl_priorities=STRING to set the following ' \
|
|
'LTL priorities:\n')
|
|
rg.dump_psl_priorities(dumpstream)
|
|
print(dumpstream.str())
|
|
print('Use argument sere_priorities=STRING to set the following ' \
|
|
'SERE priorities:\n')
|
|
rg.dump_sere_priorities(dumpstream)
|
|
print(dumpstream.str())
|
|
print('Use argument boolean_priorities=STRING to set the ' \
|
|
'following Boolean formula priorities:\n')
|
|
rg.dump_sere_bool_priorities(dumpstream)
|
|
print(dumpstream.str())
|
|
else:
|
|
sys.stderr.write("internal error: unknown type of output")
|
|
return
|
|
|
|
def _randltlgenerator(rg):
|
|
i = 0
|
|
while i != n:
|
|
f = rg.next()
|
|
if f is None:
|
|
sys.stderr.write("Warning: could not generate a new unique formula " \
|
|
"after " + str(MAX_TRIALS) + " trials.\n")
|
|
yield None
|
|
else:
|
|
yield f
|
|
i += 1
|
|
return formulaiterator(_randltlgenerator(rg))
|
|
|
|
def simplify(f, **kwargs):
|
|
level = kwargs.get('level', None)
|
|
if level is not None:
|
|
return ltl_simplifier(ltl_simplifier_options(level)).simplify(f)
|
|
|
|
basics = kwargs.get('basics', True)
|
|
synt_impl = kwargs.get('synt_impl', True)
|
|
event_univ = kwargs.get('event_univ', True)
|
|
containment_checks = kwargs.get('containment_checks', False)
|
|
containment_checks_stronger = kwargs.get('containment_checks_stronger', False)
|
|
nenoform_stop_on_boolean = kwargs.get('nenoform_stop_on_boolean', False)
|
|
reduce_size_strictly = kwargs.get('reduce_size_strictly', False)
|
|
boolean_to_isop = kwargs.get('boolean_to_isop', False)
|
|
favor_event_univ = kwargs.get('favor_event_univ', False)
|
|
|
|
simp_opts = ltl_simplifier_options(basics,
|
|
synt_impl,
|
|
event_univ,
|
|
containment_checks,
|
|
containment_checks_stronger,
|
|
nenoform_stop_on_boolean,
|
|
reduce_size_strictly,
|
|
boolean_to_isop,
|
|
favor_event_univ)
|
|
return ltl_simplifier(simp_opts).simplify(f)
|
|
|
|
for fun in dir(formula):
|
|
if (callable(getattr(formula, fun)) and
|
|
(fun[:3] == 'is_' or fun[:4] == 'has_')):
|
|
_addfilter(fun)
|
|
|
|
for fun in ['remove_x', 'get_literal', 'relabel', 'relabel_bse',
|
|
'simplify', 'unabbreviate_ltl']:
|
|
_addmap(fun)
|