1# -*- coding: utf-8 -*- 2# Copyright (C) 2014-2021 Laboratoire de 3# Recherche et Développement de l'Epita (LRDE). 4# 5# This file is part of Spot, a model checking library. 6# 7# Spot is free software; you can redistribute it and/or modify it 8# under the terms of the GNU General Public License as published by 9# the Free Software Foundation; either version 3 of the License, or 10# (at your option) any later version. 11# 12# Spot is distributed in the hope that it will be useful, but WITHOUT 13# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15# License for more details. 16# 17# You should have received a copy of the GNU General Public License 18# along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 21import sys 22 23if sys.hexversion < 0x03030000: 24 sys.exit("This module requires Python 3.3 or newer") 25 26import subprocess 27import os 28import signal 29import tempfile 30from contextlib import suppress as _supress 31 32if 'SPOT_UNINSTALLED' in os.environ: 33 # When Spot is installed, _impl.so will be in the same directory as 34 # spot/impl.py, however when we run Spot's test suite, Spot is not yet 35 # installed and we want "from . import _impl" (generated by Swig4) to look 36 # into .libs/ 37 __path__.extend(sys.path) 38 39# We may have third-party plugins that want to be loaded as "spot.xxx", but 40# that are installed in a different $prefix. This sets things so that any 41# file that looks like spot-extra/xxx.py can be loaded with "import spot.xxx". 42for path in sys.path: 43 if path not in __path__: 44 path += "/spot-extra" 45 if os.path.isdir(path): 46 __path__.append(path) 47 48 49from spot.impl import * 50# spot.aux_ used to be called spot.aux until the filename aux.py 51# caused issues on Windows. So the file is now named aux_.py, but we 52# still want to import it as spot.aux, hence we add it to spot.modules 53# as an alias. 54import spot.aux_ as aux 55sys.modules['spot.aux'] = aux 56from spot.aux import \ 57 extend as _extend, \ 58 str_to_svg as _str_to_svg, \ 59 ostream_to_svg as _ostream_to_svg 60 61 62# The parrameters used by default when show() is called on an automaton. 63_show_default = None 64 65 66def setup(**kwargs): 67 """Configure Spot for fancy display. 68 69 This is manly useful in Jupyter/IPython. 70 71 Note that this function needs to be called before any automaton is 72 displayed. Afterwards it will have no effect (you should restart 73 Python, or the Jupyter/IPython Kernel). 74 75 Parameters 76 ---------- 77 bullets : bool 78 whether to display acceptance conditions as UTF8 bullets 79 (default: True) 80 fillcolor : str 81 the color to use for states (default: '#ffffaa') 82 size : str 83 the width and height of the GraphViz output in inches 84 (default: '10.2,5') 85 font : str 86 the font to use in the GraphViz output (default: 'Lato') 87 show_default : str 88 default options for show() 89 max_states : int 90 maximum number of states in GraphViz output (default: 50) 91 """ 92 import os 93 94 s = ('size="{}" edge[arrowhead=vee, arrowsize=.7]') 95 os.environ['SPOT_DOTEXTRA'] = s.format(kwargs.get('size', '10.13,5')) 96 97 bullets = 'B' if kwargs.get('bullets', True) else '' 98 max_states = '<' + str(kwargs.get('max_states', 50)) 99 d = 'rf({})C({}){}'.format(kwargs.get('font', 'Lato'), 100 kwargs.get('fillcolor', '#ffffaa'), 101 bullets + max_states) 102 global _show_default 103 _show_default = kwargs.get('show_default', None) 104 os.environ['SPOT_DOTDEFAULT'] = d 105 106 107# In version 3.0.2, Swig puts strongly typed enum in the main 108# namespace without prefixing them. Latter versions fix this. So we 109# can remove for following hack once 3.0.2 is no longer used in our 110# build farm. 111if 'op_ff' not in globals(): 112 for i in ('ff', 'tt', 'eword', 'ap', 'Not', 'X', 'F', 'G', 113 'Closure', 'NegClosure', 'NegClosureMarked', 114 'Xor', 'Implies', 'Equiv', 'U', 'R', 'W', 'M', 115 'EConcat', 'EConcatMarked', 'UConcat', 'Or', 116 'OrRat', 'And', 'AndRat', 'AndNLM', 'Concat', 117 'Fusion', 'Star', 'FStar'): 118 globals()['op_' + i] = globals()[i] 119 del globals()[i] 120 121 122# Global BDD dict so that we do not have to create one in user code. 123_bdd_dict = make_bdd_dict() 124 125 126__om_init_tmp = option_map.__init__ 127 128 129def __om_init_new(self, str=None): 130 __om_init_tmp(self) 131 if str: 132 res = self.parse_options(str) 133 if res: 134 raise RuntimeError("failed to parse option at: '" + str + "'") 135 136 137option_map.__init__ = __om_init_new 138 139@_extend(aig) 140class aig: 141 def _repr_svg_(self, opt=None): 142 ostr = ostringstream() 143 print_dot(ostr, self, opt) 144 return _ostream_to_svg(ostr) 145 146 def show(self, opt=None): 147 from spot.jupyter import SVG 148 return SVG(self._repr_svg_(opt)) 149 150 def to_str(self, format='circuit', opt=None): 151 format = format.lower() 152 if format == 'circuit': 153 ostr = ostringstream() 154 print_aiger(ostr, self) 155 return ostr.str() 156 if format == 'dot': 157 ostr = ostringstream() 158 print_dot(ostr, self, opt) 159 return ostr.str() 160 raise ValueError("unknown string format: " + format) 161 162 def evaluate(self, gen): 163 self.circ_init() 164 outputs_pos = self.outputs() 165 out_names = self.output_names() 166 for x in gen: 167 if len(x) != self.num_inputs(): 168 raise ValueError("Incorrect number of inputs") 169 self.circ_step(x) 170 values = self.circ_state() 171 res_val = [values[index] for index in outputs_pos] 172 assert(len(res_val) == len(out_names)) 173 yield list(zip(out_names, res_val)) 174 175__twa__acc1 = twa.acc 176__twa__acc2 = twa.get_acceptance 177 178 179# We store the automaton into the acceptance condition 180# returned by acc so that it does not crash when 181# taking the reference to a temporary, as in 182# spot.translate('Foo').acc() 183# Issue #468. 184def __twa_acc1_tmp(self): 185 a = __twa__acc1(self) 186 a._aut = self 187 return a 188 189 190def __twa_acc2_tmp(self): 191 a = __twa__acc2(self) 192 a._aut = self 193 return a 194 195 196twa.acc = __twa_acc1_tmp 197twa.get_acceptance = __twa_acc2_tmp 198 199 200@_extend(twa, ta) 201class twa: 202 def _repr_svg_(self, opt=None): 203 """Output the automaton as SVG""" 204 ostr = ostringstream() 205 if opt is None: 206 global _show_default 207 opt = _show_default 208 print_dot(ostr, self, opt) 209 return _ostream_to_svg(ostr) 210 211 def show(self, opt=None): 212 """Display the automaton as SVG, in the IPython/Jupyter notebook""" 213 if opt is None: 214 global _show_default 215 opt = _show_default 216 # Load the SVG function only if we need it. This way the 217 # bindings can still be used outside of IPython if IPython is 218 # not installed. 219 from spot.jupyter import SVG 220 return SVG(self._repr_svg_(opt)) 221 222 def highlight_states(self, states, color): 223 """Highlight a list of states. This can be a list of 224 state numbers, or a list of Booleans.""" 225 for idx, val in enumerate(states): 226 if type(val) is bool: 227 if val: 228 self.highlight_state(idx, color) 229 else: 230 self.highlight_state(val, color) 231 return self 232 233 def highlight_edges(self, edges, color): 234 """Highlight a list of edges. This can be a list of 235 edge numbers, or a list of Booleans.""" 236 for idx, val in enumerate(edges): 237 if type(val) is bool: 238 if val: 239 self.highlight_edge(idx, color) 240 else: 241 self.highlight_edge(val, color) 242 return self 243 244@_extend(twa) 245class twa: 246 def to_str(a, format='hoa', opt=None): 247 format = format.lower() 248 if format == 'hoa': 249 ostr = ostringstream() 250 print_hoa(ostr, a, opt) 251 return ostr.str() 252 if format == 'dot': 253 ostr = ostringstream() 254 print_dot(ostr, a, opt) 255 return ostr.str() 256 if format == 'spin': 257 ostr = ostringstream() 258 print_never_claim(ostr, a, opt) 259 return ostr.str() 260 if format == 'lbtt': 261 ostr = ostringstream() 262 print_lbtt(ostr, a, opt) 263 return ostr.str() 264 raise ValueError("unknown string format: " + format) 265 266 def save(a, filename, format='hoa', opt=None, append=False): 267 with open(filename, 'a' if append else 'w') as f: 268 s = a.to_str(format, opt) 269 f.write(s) 270 if s[-1] != '\n': 271 f.write('\n') 272 return a 273 274 275@_extend(twa_graph) 276class twa_graph: 277 def show_storage(self, opt=None): 278 ostr = ostringstream() 279 self.dump_storage_as_dot(ostr, opt) 280 from spot.jupyter import SVG 281 return SVG(_ostream_to_svg(ostr)) 282 283 def __copy__(self): 284 return make_twa_graph(self, twa_prop_set.all(), True) 285 286 287def make_twa_graph(*args): 288 from spot.impl import make_twa_graph as mtg 289 if len(args) == 0: 290 return mtg(_bdd_dict) 291 return mtg(*args) 292 293 294@_extend(formula) 295class formula: 296 def __init__(self, str): 297 """Parse the given string to create a formula.""" 298 if type(str) == formula: 299 self.this = str 300 else: 301 self.this = parse_formula(str) 302 303 def show_ast(self): 304 """Display the syntax tree of the formula.""" 305 # Load the SVG function only if we need it. This way the bindings 306 # can still be used outside of IPython if IPython is not 307 # installed. 308 from spot.jupyter import SVG 309 return SVG(_str_to_svg(self.to_str('d'))) 310 311 def _repr_latex_(self): 312 return '$' + self.to_str('j') + '$' 313 314 def to_str(self, format='spot', parenth=False): 315 if format == 'spot' or format == 'f': 316 return str_psl(self, parenth) 317 elif format == 'spin' or format == 's': 318 return str_spin_ltl(self, parenth) 319 elif format == 'utf8' or format == '8': 320 return str_utf8_psl(self, parenth) 321 elif format == 'lbt' or format == 'l': 322 return str_lbt_ltl(self) 323 elif format == 'wring' or format == 'w': 324 return str_wring_ltl(self) 325 elif format == 'latex' or format == 'x': 326 return str_latex_psl(self, parenth) 327 elif format == 'sclatex' or format == 'X': 328 return str_sclatex_psl(self, parenth) 329 elif format == 'mathjax' or format == 'j': 330 return (str_sclatex_psl(self, parenth). 331 replace("``", "\\unicode{x201C}"). 332 replace("\\textrm{''}", "\\unicode{x201D}")) 333 elif format == 'dot' or format == 'd': 334 ostr = ostringstream() 335 print_dot_psl(ostr, self) 336 return ostr.str().encode('utf-8') 337 else: 338 raise ValueError("unknown string format: " + format) 339 340 def __format__(self, spec): 341 """Format the formula according to `spec`. 342 343 Parameters 344 ---------- 345 spec : str, optional 346 a list of letters that specify how the formula 347 should be formatted. 348 349 Supported specifiers 350 -------------------- 351 352 - 'f': use Spot's syntax (default) 353 - '8': use Spot's syntax in UTF-8 mode 354 - 's': use Spin's syntax 355 - 'l': use LBT's syntax 356 - 'w': use Wring's syntax 357 - 'x': use LaTeX output 358 - 'X': use self-contained LaTeX output 359 - 'j': use self-contained LaTeX output, adjusted for MathJax 360 361 Add some of those letters for additional options: 362 363 - 'p': use full parentheses 364 - 'c': escape the formula for CSV output (this will 365 enclose the formula in double quotes, and escape 366 any included double quotes) 367 - 'h': escape the formula for HTML output 368 - 'd': escape double quotes and backslash, 369 for use in C-strings (the outermost double 370 quotes are *not* added) 371 - 'q': quote and escape for shell output, using single 372 quotes or double quotes depending on the contents. 373 - '[...]': rewrite away all the operators specified in brackets, 374 using spot.unabbreviate(). 375 376 - ':spec': pass the remaining specification to the 377 formating function for strings. 378 379 """ 380 381 syntax = 'f' 382 parent = False 383 escape = None 384 385 form = self 386 387 while spec: 388 c, spec = spec[0], spec[1:] 389 if c in ('f', 's', '8', 'l', 'w', 'x', 'X', 'j'): 390 syntax = c 391 elif c == 'p': 392 parent = True 393 elif c in ('c', 'd', 'h', 'q'): 394 escape = c 395 elif c == ':': 396 break 397 elif c == '[': 398 pos = spec.find(']') 399 if pos < 0: 400 raise ValueError("unclosed bracket: [" + spec) 401 form = form.unabbreviate(spec[0:pos]) 402 spec = spec[pos+1:] 403 else: 404 raise ValueError("unknown format specification: " + c + spec) 405 406 s = form.to_str(syntax, parent) 407 408 if escape == 'c': 409 o = ostringstream() 410 escape_rfc4180(o, s) 411 s = '"' + o.str() + '"' 412 elif escape == 'd': 413 s = escape_str(s) 414 elif escape == 'h': 415 o = ostringstream() 416 escape_html(o, s) 417 s = o.str() 418 elif escape == 'q': 419 o = ostringstream() 420 quote_shell_string(o, s) 421 s = o.str() 422 423 return s.__format__(spec) 424 425 def traverse(self, func, *args): 426 if func(self, *args): 427 return 428 for f in self: 429 f.traverse(func, *args) 430 431 def map(self, func, *args): 432 k = self.kind() 433 if k in (op_ff, op_tt, op_eword, op_ap): 434 return self 435 if k in (op_Not, op_X, op_F, op_G, op_Closure, 436 op_NegClosure, op_NegClosureMarked): 437 return formula.unop(k, func(self[0], *args)) 438 if k in (op_Xor, op_Implies, op_Equiv, op_U, op_R, op_W, 439 op_M, op_EConcat, op_EConcatMarked, op_UConcat): 440 return formula.binop(k, func(self[0], *args), func(self[1], *args)) 441 if k in (op_Or, op_OrRat, op_And, op_AndRat, op_AndNLM, 442 op_Concat, op_Fusion): 443 return formula.multop(k, [func(x, *args) for x in self]) 444 if k in (op_Star, op_FStar): 445 return formula.bunop(k, func(self[0], *args), 446 self.min(), self.max()) 447 raise ValueError("unknown type of formula") 448 449 450@_extend(atomic_prop_set) 451class atomic_prop_set: 452 def _repr_latex_(self): 453 res = '$\{' 454 comma = '' 455 for ap in self: 456 apname = ap.to_str('j') 457 if not '\\unicode{' in apname: 458 apname = "\\unicode{x201C}" + apname + "\\unicode{x201D}" 459 res += comma 460 comma = ', ' 461 res += apname 462 res += '\}$' 463 return res 464 465 466@_extend(zielonka_tree) 467class zielonka_tree: 468 def _repr_svg_(self): 469 """Output the Zielonka tree as SVG""" 470 ostr = ostringstream() 471 self.dot(ostr) 472 return _ostream_to_svg(ostr) 473 474_acdnum = 0 475 476@_extend(acd) 477class acd: 478 def _repr_svg_(self, id=None): 479 """Output the ACD as SVG""" 480 ostr = ostringstream() 481 self.dot(ostr, id) 482 return _ostream_to_svg(ostr) 483 484 def _repr_html_(self): 485 global _acdnum 486 num = _acdnum 487 _acdnum += 1 488 style = ''' 489.acdhigh ellipse,.acdacc ellipse,.acdacc path,.acdacc polygon{stroke:green;} 490.acdhigh polygon,.acdrej ellipse,.acdrej path,.acdrej polygon{stroke:red;} 491.acdbold ellipse,.acdbold polygon,.acdbold path{stroke-width:2;} 492.acdrej polygon{fill:red;} 493.acdacc polygon{fill:green;} 494''' 495 js = ''' 496function acd{num}_clear(){{ 497 $("#acd{num} .node,#acdaut{num} .node,#acdaut{num} .edge") 498 .removeClass("acdhigh acdbold acdacc acdrej"); 499}}; 500function acd{num}_state(state){{ 501 acd{num}_clear(); 502 $("#acd{num} .acdS" + state).addClass("acdhigh acdbold"); 503 $("#acdaut{num} #S" + state).addClass("acdbold"); 504}}; 505function acd{num}_edge(edge){{ 506 acd{num}_clear(); 507 var theedge = $('#acdaut{num} #E' + edge) 508 var classList = theedge.attr('class').split(/\s+/); 509 $.each(classList, function(index, item) {{ 510 if (item.startsWith('acdN')) {{ 511 $("#acd{num} #" + item.substring(3)).addClass("acdhigh acdbold"); 512 }} 513 }}); 514 theedge.addClass("acdbold"); 515}}; 516function acd{num}_node(node, acc){{ 517 acd{num}_clear(); 518 $("#acdaut{num} .acdN" + node).addClass(acc 519 ? "acdacc acdbold" 520 : "acdrej acdbold"); 521 $("#acd{num} #N" + node).addClass("acdbold acdhigh"); 522}};'''.format(num=num) 523 me = 0 524 for n in range(self.node_count()): 525 for e in self.edges_of_node(n): 526 me = max(e, me) 527 js += '$("#acdaut{num} #E{e}").addClass("acdN{n}");'\ 528 .format(num=num, e=e, n=n) 529 for e in range(1, me + 1): 530 js += '$("#acdaut{num} #E{e}")'\ 531 '.click(function(){{acd{num}_edge({e});}});'\ 532 .format(num=num, e=e) 533 for s in range(self.get_aut().num_states()): 534 js += '$("#acdaut{num} #S{s}")'\ 535 '.click(function(){{acd{num}_state({s});}});'\ 536 .format(num=num, s=s) 537 for n in range(self.node_count()): 538 v = int(self.node_acceptance(n)) 539 js += '$("#acd{num} #N{n}")'\ 540 '.click(function(){{acd{num}_node({n}, {v});}});'\ 541 .format(num=num, n=n, v=v) 542 html = '<style>{}</style><div>{}</div><div>{}</div><script>{}</script>'\ 543 .format(style, 544 self.get_aut().show('.i(acdaut{})'.format(num)).data, 545 self._repr_svg_("acd{}".format(num)), 546 js); 547 return html 548 549 550def automata(*sources, timeout=None, ignore_abort=True, 551 trust_hoa=True, no_sid=False, debug=False, 552 want_kripke=False): 553 """Read automata from a list of sources. 554 555 Parameters 556 ---------- 557 *sources : list of str 558 These sources can be either commands (end with `|`), 559 textual representations of automata (contain `\n`), 560 or filenames (else). 561 timeout : int, optional 562 Number of seconds to wait for the result of a command. 563 If None (the default), not limit is used. 564 ignore_abort : bool, optional 565 If True (the default), skip HOA atomata that ends with 566 `--ABORT--`, and return the next automaton in the stream. 567 If False, aborted automata are reported as syntax errors. 568 trust_hoa : bool, optional 569 If True (the default), supported HOA properies that 570 cannot be easily verified are trusted. 571 want_kripke : bool, optional 572 If True, the input is expected to discribe Kripke 573 structures, in the HOA format, and the returned type 574 will be of type kripke_graph_ptr. 575 no_sid : bool, optional 576 When an automaton is obtained from a subprocess, this 577 subprocess is started from a shell with its own session 578 group (the default) unless no_sid is set to True. 579 debug : bool, optional 580 Whether to run the parser in debug mode. 581 582 Notes 583 ----- 584 585 The automata can be written in the `HOA format`_, as `never 586 claims`_, in `LBTT's format`_, or in `ltl2dstar's format`_. 587 588 .. _HOA format: http://adl.github.io/hoaf/ 589 .. _never claims: http://spinroot.com/spin/Man/never.html 590 .. _LBTT's format: 591 http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html 592 .. _ltl2dstar's format: 593 http://www.ltl2dstar.de/docs/ltl2dstar.html#output-format-dstar 594 595 If an argument ends with a `|`, then this argument is interpreted as 596 a shell command, and the output of that command (without the `|`) 597 is parsed. 598 599 If an argument contains a newline, then it is interpreted as 600 actual contents to be parsed. 601 602 Otherwise, the argument is assumed to be a filename. 603 604 The result of this function is a generator on all the automata 605 objects read from these sources. The typical usage is:: 606 607 for aut in spot.automata(filename, command, ...): 608 # do something with aut 609 610 When the source is a command, and no `timeout` is specified, 611 parsing is done straight out of the pipe connecting the 612 command. So 613 614 for aut in spot.automata('randaut -H -n 10 2 |'): 615 process(aut) 616 617 will call `process(aut)` on each automaton as soon as it is output by 618 `randaut`, and without waiting for `randaut` to terminate. 619 620 However if `timeout` is passed, then `automata()` will wait for 621 the entire command to terminate before parsing its entire output. 622 If one command takes more than `timeout` seconds, 623 `subprocess.TimeoutExpired` is raised. 624 625 If any command terminates with a non-zero error, 626 `subprocess.CalledProcessError` is raised. 627 """ 628 629 o = automaton_parser_options() 630 o.debug = debug 631 o.ignore_abort = ignore_abort 632 o.trust_hoa = trust_hoa 633 o.raise_errors = True 634 o.want_kripke = want_kripke 635 636 for filename in sources: 637 try: 638 p = None 639 proc = None 640 if filename[-1] == '|': 641 setsid_maybe = None 642 if not no_sid: 643 setsid_maybe = os.setsid 644 # universal_newlines for str output instead of bytes 645 # when the pipe is read from Python (which happens 646 # when timeout is set). 647 prefn = None if no_sid else os.setsid 648 proc = subprocess.Popen(filename[:-1], shell=True, 649 preexec_fn=prefn, 650 universal_newlines=True, 651 stdout=subprocess.PIPE) 652 if timeout is None: 653 p = automaton_stream_parser(proc.stdout.fileno(), 654 filename, o) 655 else: 656 try: 657 out, err = proc.communicate(timeout=timeout) 658 except subprocess.TimeoutExpired: 659 # Using subprocess.check_output() with timeout 660 # would just kill the shell, not its children. 661 os.killpg(proc.pid, signal.SIGKILL) 662 raise 663 else: 664 ret = proc.wait() 665 if ret: 666 raise subprocess.CalledProcessError(ret, 667 filename[:-1]) 668 finally: 669 proc = None 670 p = automaton_stream_parser(out, filename, o) 671 elif '\n' in filename: 672 p = automaton_stream_parser(filename, "<string>", o) 673 else: 674 p = automaton_stream_parser(filename, o) 675 a = True 676 # Using proc as a context manager ensures that proc.stdout will be 677 # closed on exit, and the process will be properly waited for. 678 # This is important when running tools that produce an infinite 679 # stream of automata and that must be killed once the generator 680 # returned by spot.automata() is destroyed. Otherwise, _supress() 681 # is just a dummy context manager that does nothing (Python 3.7 682 # introduces nullcontext() for this purpose, but at the time of 683 # writing we support Python 3.4). 684 mgr = proc if proc else _supress() 685 with mgr: 686 while a: 687 # the automaton is None when we reach the end of the file. 688 res = p.parse(_bdd_dict) 689 a = res.ks if want_kripke else res.aut 690 if a: 691 yield a 692 finally: 693 # Make sure we destroy the parser (p) and the subprocess 694 # (prop) in the correct order. 695 del p 696 if proc is not None: 697 ret = proc.returncode 698 del proc 699 # Do not complain about the exit code if we are already raising 700 # an exception. 701 if ret and sys.exc_info()[0] is None: 702 raise subprocess.CalledProcessError(ret, filename[:-1]) 703 # deleting o explicitly now prevents Python 3.5 from 704 # reporting the following error: "<built-in function 705 # delete_automaton_parser_options> returned a result with 706 # an error set". It's not clear to me if the bug is in Python 707 # or Swig. At least it's related to the use of generators. 708 del o 709 return 710 711 712def automaton(filename, **kwargs): 713 """Read a single automaton from a file. 714 715 See `spot.automata` for a list of supported formats.""" 716 try: 717 return next(automata(filename, **kwargs)) 718 except StopIteration: 719 raise RuntimeError("Failed to read automaton from {}".format(filename)) 720 721def aiger_circuits(*sources, bdd_dict = None): 722 """Read aiger circuits from a list of sources. 723 724 Parameters 725 ---------- 726 *sources : list of str 727 These sources can be either commands (end with `|`), 728 textual representations of the circuit in restricted aag format 729 (start with aag and contain '\n'), or filenames (else). 730 bdd_dict : If not supplied, a fresh bdd_dict will be created, common for 731 all of the circuits. 732 """ 733 734 bdd_dict = bdd_dict if bdd_dict is not None else make_bdd_dict() 735 736 for source in sources: 737 if (source.startswith("aag") and '\n' in source): 738 yield aig.parse_aag(source, "<string>", bdd_dict) 739 else: 740 yield aig.parse_aag(source, bdd_dict) 741 742def aiger_circuit(source, bdd_dict = None): 743 """Read a single aiger circuit from file or textual representation. 744 745 See `spot.aiger_circuits` for a list of supported formats.""" 746 try: 747 return next(aiger_circuits(source, bdd_dict = bdd_dict)) 748 except StopIteration: 749 raise RuntimeError("Failed to read an aiger circuit " 750 "from {}".format(source)) 751 752 753def _postproc_translate_options(obj, default_type, *args): 754 type_name_ = None 755 type_ = None 756 pref_name_ = None 757 pref_ = None 758 optm_name_ = None 759 optm_ = None 760 comp_ = 0 761 unam_ = 0 762 sbac_ = 0 763 colo_ = 0 764 765 def type_set(val): 766 nonlocal type_, type_name_ 767 if type_ is not None and type_name_ != val: 768 raise ValueError("type cannot be both {} and {}" 769 .format(type_name_, val)) 770 elif val == 'generic' or val == 'gen' or val == 'g': 771 type_ = postprocessor.Generic 772 elif val == 'tgba': # historical 773 type_ = postprocessor.GeneralizedBuchi 774 elif val == 'generalizedbuchi': 775 type_ = postprocessor.GeneralizedBuchi 776 elif val == 'ba': # historical 777 type_ = postprocessor.Buchi 778 sbac_ = postprocessor.SBAcc 779 elif val == 'buchi': 780 type_ = postprocessor.Buchi 781 elif val == 'cobuchi' or val == 'nca': 782 type_ = postprocessor.CoBuchi 783 elif val == 'dca': 784 type_ = postprocessor.CoBuchi 785 pref_ = postprocessor.Deterministic 786 elif val == 'parity min odd': 787 type_ = postprocessor.ParityMinOdd 788 elif val == 'parity min even': 789 type_ = postprocessor.ParityMinEven 790 elif val == 'parity max odd': 791 type_ = postprocessor.ParityMaxOdd 792 elif val == 'parity max even': 793 type_ = postprocessor.ParityMaxEven 794 elif val == 'parity min': 795 type_ = postprocessor.ParityMin 796 elif val == 'parity max': 797 type_ = postprocessor.ParityMax 798 elif val == 'parity odd': 799 type_ = postprocessor.ParityOdd 800 elif val == 'parity even': 801 type_ = postprocessor.ParityEven 802 elif val == 'parity': 803 type_ = postprocessor.Parity 804 else: 805 assert(val == 'monitor') 806 type_ = postprocessor.Monitor 807 type_name_ = val 808 809 def pref_set(val): 810 nonlocal pref_, pref_name_ 811 if pref_ is not None and pref_name_ != val: 812 raise ValueError("preference cannot be both {} and {}" 813 .format(pref_name_, val)) 814 elif val == 'small': 815 pref_ = postprocessor.Small 816 elif val == 'deterministic': 817 pref_ = postprocessor.Deterministic 818 else: 819 assert(val == 'any') 820 pref_ = postprocessor.Any 821 pref_name_ = val 822 823 def optm_set(val): 824 nonlocal optm_, optm_name_ 825 if optm_ is not None and optm_name_ != val: 826 raise ValueError("optimization level cannot be both {} and {}" 827 .format(optm_name_, val)) 828 if val == 'high': 829 optm_ = postprocessor.High 830 elif val.startswith('med'): 831 optm_ = postprocessor.Medium 832 else: 833 assert(val == 'low') 834 optm_ = postprocessor.Low 835 optm_name_ = val 836 837 def misc_set(val): 838 nonlocal comp_, unam_, sbac_, colo_ 839 if val == 'colored': 840 colo_ = postprocessor.Colored 841 elif val == 'complete': 842 comp_ = postprocessor.Complete 843 elif (val == 'sbacc' or val == 'statebasedacceptance' 844 or val == 'state-based-acceptance'): 845 sbac_ = postprocessor.SBAcc 846 else: 847 assert(val == 'unambiguous') 848 unam_ = postprocessor.Unambiguous 849 850 options = { 851 'any': pref_set, 852 'ba': type_set, 853 'buchi': type_set, 854 'cobuchi': type_set, 855 'colored': misc_set, 856 'complete': misc_set, 857 'dca': type_set, 858 'deterministic': pref_set, 859 'g': type_set, 860 'gen': type_set, 861 'generic': type_set, 862 'generalizedbuchi': type_set, 863 'high': optm_set, 864 'low': optm_set, 865 'medium': optm_set, 866 'monitor': type_set, 867 'nca': type_set, 868 'parity even': type_set, 869 'parity max even': type_set, 870 'parity max odd': type_set, 871 'parity max': type_set, 872 'parity min even': type_set, 873 'parity min odd': type_set, 874 'parity min': type_set, 875 'parity odd': type_set, 876 'parity': type_set, 877 'sbacc': misc_set, 878 'small': pref_set, 879 'statebasedacceptance': misc_set, 880 'state-based-acceptance': misc_set, 881 'tgba': type_set, 882 'unambiguous': misc_set, 883 } 884 885 for arg in args: 886 arg = arg.lower() 887 fn = options.get(arg) 888 if fn: 889 fn(arg) 890 else: 891 # arg is not an know option, but maybe it is a prefix of 892 # one of them 893 compat = [] 894 f = None 895 for key, fn in options.items(): 896 if key.startswith(arg): 897 compat.append(key) 898 f = fn 899 lc = len(compat) 900 if lc == 1: 901 f(compat[0]) 902 elif lc < 1: 903 raise ValueError("unknown option '{}'".format(arg)) 904 else: 905 raise ValueError("ambiguous option '{}' is prefix of {}" 906 .format(arg, str(compat))) 907 908 if type_ is None: 909 type_ = default_type 910 if pref_ is None: 911 pref_ = postprocessor.Small 912 if optm_ is None: 913 optm_ = postprocessor.High 914 915 obj.set_type(type_) 916 obj.set_pref(pref_ | comp_ | unam_ | sbac_ | colo_) 917 obj.set_level(optm_) 918 919 920def translate(formula, *args, dict=_bdd_dict, xargs=None): 921 """Translate a formula into an automaton. 922 923 Keep in mind that 'Deterministic' expresses just a preference that 924 may not be satisfied. 925 926 The optional arguments should be strings among the following: 927 - at most one in 'GeneralizedBuchi', 'Buchi', or 'Monitor', 928 'generic', 'parity', 'parity min odd', 'parity min even', 929 'parity max odd', 'parity max even', 'coBuchi' 930 (type of acceptance condition to build) 931 - at most one in 'Small', 'Deterministic', 'Any' 932 (preferred characteristics of the produced automaton) 933 - at most one in 'Low', 'Medium', 'High' 934 (optimization level) 935 - any combination of 'Complete', 'Unambiguous', 936 'StateBasedAcceptance' (or 'SBAcc' for short), and 937 'Colored' (only for parity acceptance) 938 939 The default corresponds to 'tgba', 'small' and 'high'. 940 941 Additional options can be supplied using a `spot.option_map`, or a 942 string (that will be converted to `spot.option_map`), as the `xargs` 943 argument. This is similar to the `-x` option of command-line tools; 944 so check out the spot-x(7) man page for details. 945 946 """ 947 if type(xargs) is str: 948 xargs = option_map(xargs) 949 a = translator(dict, xargs) 950 _postproc_translate_options(a, postprocessor.TGBA, *args) 951 if type(formula) == str: 952 formula = parse_formula(formula) 953 result = a.run(formula) 954 if xargs: 955 xargs.report_unused_options() 956 return result 957 958 959formula.translate = translate 960 961 962# Wrap C++-functions into lambdas so that they get converted into 963# instance methods (i.e., self passed as first argument 964# automatically), because only user-defined functions are converted as 965# instance methods. 966def _add_formula(meth, name=None): 967 setattr(formula, name or meth, (lambda self, *args, **kwargs: 968 globals()[meth](self, *args, **kwargs))) 969 970 971_add_formula('contains') 972_add_formula('are_equivalent', 'equivalent_to') 973 974 975def postprocess(automaton, *args, formula=None, xargs=None): 976 """Post process an automaton. 977 978 This applies a number of simplification algorithms, depending on 979 the options supplied. Keep in mind that 'Deterministic' expresses 980 just a preference that may not be satisfied if the input is 981 not already 'Deterministic'. 982 983 The optional arguments should be strings among the following: 984 - at most one in 'Generic', 'GeneralizedBuchi', 'Buchi', or 985 'Monitor', 'parity', 'parity min odd', 'parity min even', 986 'parity max odd', 'parity max even', 'coBuchi' 987 (type of acceptance condition to build) 988 - at most one in 'Small', 'Deterministic', 'Any' 989 (preferred characteristics of the produced automaton) 990 - at most one in 'Low', 'Medium', 'High' 991 (optimization level) 992 - any combination of 'Complete', 'StateBasedAcceptance' 993 (or 'SBAcc' for short), and 'Colored (only for parity 994 acceptance) 995 996 The default corresponds to 'generic', 'small' and 'high'. 997 998 If a formula denoted by this automaton is known, pass it to as the 999 optional `formula` argument; it can help some algorithms by 1000 providing an easy way to complement the automaton. 1001 1002 Additional options can be supplied using a `spot.option_map`, or a 1003 string (that will be converted to `spot.option_map`), as the `xargs` 1004 argument. This is similar to the `-x` option of command-line tools; 1005 so check out the spot-x(7) man page for details. 1006 1007 """ 1008 if type(xargs) is str: 1009 xargs = option_map(xargs) 1010 p = postprocessor(xargs) 1011 if type(automaton) == str: 1012 automaton = globals()['automaton'](automaton) 1013 _postproc_translate_options(p, postprocessor.Generic, *args) 1014 result = p.run(automaton, formula) 1015 if xargs: 1016 xargs.report_unused_options() 1017 return result 1018 1019 1020twa.postprocess = postprocess 1021 1022 1023# Wrap C++-functions into lambdas so that they get converted into 1024# instance methods (i.e., self passed as first argument 1025# automatically), because only user-defined functions are converted as 1026# instance methods. 1027def _add_twa_graph(meth, name=None): 1028 setattr(twa_graph, name or meth, (lambda self, *args, **kwargs: 1029 globals()[meth](self, *args, **kwargs))) 1030 1031 1032for meth in ('scc_filter', 'scc_filter_states', 1033 'is_deterministic', 'is_unambiguous', 1034 'contains', 'get_strategy', 1035 'set_state_players', 'get_state_players', 1036 'set_state_player', 'get_state_player', 1037 'get_state_winners', 'get_state_winner'): 1038 _add_twa_graph(meth) 1039_add_twa_graph('are_equivalent', 'equivalent_to') 1040 1041# Wrapper around a formula iterator to which we add some methods of formula 1042# (using _addfilter and _addmap), so that we can write things like 1043# formulas.simplify().is_X_free(). 1044 1045 1046class formulaiterator: 1047 def __init__(self, formulas): 1048 self._formulas = formulas 1049 1050 def __iter__(self): 1051 return self 1052 1053 def __next__(self): 1054 return next(self._formulas) 1055 1056 1057# fun shoud be a predicate and should be a method of formula. 1058# _addfilter adds this predicate as a filter whith the same name in 1059# formulaiterator. 1060def _addfilter(fun): 1061 def filtf(self, *args, **kwargs): 1062 it = filter(lambda f: getattr(f, fun)(*args, **kwargs), self) 1063 return formulaiterator(it) 1064 1065 def nfiltf(self, *args, **kwargs): 1066 it = filter(lambda f: not getattr(f, fun)(*args, **kwargs), self) 1067 return formulaiterator(it) 1068 1069 if fun[:3] == 'is_': 1070 notfun = 'is_not_' + fun[3:] 1071 elif fun[:4] == 'has_': 1072 notfun = 'has_no_' + fun[4:] 1073 else: 1074 notfun = 'not_' + fun 1075 setattr(formulaiterator, fun, filtf) 1076 setattr(formulaiterator, notfun, nfiltf) 1077 1078 1079# fun should be a function taking a formula as its first parameter and 1080# returning a formula. _addmap adds this function as a method of 1081# formula and formulaiterator. 1082def _addmap(fun): 1083 def mapf(self, *args, **kwargs): 1084 return formulaiterator(map(lambda f: getattr(f, fun)(*args, **kwargs), 1085 self)) 1086 setattr(formula, fun, 1087 lambda self, *args, **kwargs: 1088 globals()[fun](self, *args, **kwargs)) 1089 setattr(formulaiterator, fun, mapf) 1090 1091 1092def randltl(ap, n=-1, **kwargs): 1093 """Generate random formulas. 1094 1095 Returns a random formula iterator. 1096 1097 ap: the number of atomic propositions used to generate random formulas. 1098 1099 n: number of formulas to generate, or unbounded if n < 0. 1100 1101 **kwargs: 1102 seed: seed for the random number generator (0). 1103 output: can be 'ltl', 'psl', 'bool' or 'sere' ('ltl'). 1104 allow_dups: allow duplicate formulas (False). 1105 tree_size: tree size of the formulas generated, before mandatory 1106 simplifications (15) 1107 boolean_priorities: set priorities for Boolean formulas. 1108 ltl_priorities: set priorities for LTL formulas. 1109 sere_priorities: set priorities for SERE formulas. 1110 dump_priorities: show current priorities, do not generate any formula. 1111 simplify: 1112 0 No rewriting 1113 1 basic rewritings and eventual/universal rules 1114 2 additional syntactic implication rules 1115 3 (default) better implications using containment 1116 """ 1117 opts = option_map() 1118 output_map = { 1119 "ltl": randltlgenerator.LTL, 1120 "psl": randltlgenerator.PSL, 1121 "bool": randltlgenerator.Bool, 1122 "sere": randltlgenerator.SERE 1123 } 1124 1125 if isinstance(ap, list): 1126 aprops = atomic_prop_set() 1127 for elt in ap: 1128 aprops.insert(formula.ap(elt)) 1129 ap = aprops 1130 ltl_priorities = kwargs.get("ltl_priorities", None) 1131 sere_priorities = kwargs.get("sere_priorities", None) 1132 boolean_priorities = kwargs.get("boolean_priorities", None) 1133 output = output_map[kwargs.get("output", "ltl")] 1134 opts.set("output", output) 1135 opts.set("seed", kwargs.get("seed", 0)) 1136 tree_size = kwargs.get("tree_size", 15) 1137 if isinstance(tree_size, tuple): 1138 tree_size_min, tree_size_max = tree_size 1139 else: 1140 tree_size_min = tree_size_max = tree_size 1141 opts.set("tree_size_min", tree_size_min) 1142 opts.set("tree_size_max", tree_size_max) 1143 opts.set("unique", not kwargs.get("allow_dups", False)) 1144 opts.set("wf", kwargs.get("weak_fairness", False)) 1145 simpl_level = kwargs.get("simplify", 0) 1146 if simpl_level > 3 or simpl_level < 0: 1147 sys.stderr.write('invalid simplification level: ' + simpl_level) 1148 return 1149 opts.set("simplification_level", simpl_level) 1150 1151 rg = randltlgenerator(ap, opts, ltl_priorities, sere_priorities, 1152 boolean_priorities) 1153 1154 dump_priorities = kwargs.get("dump_priorities", False) 1155 if dump_priorities: 1156 dumpstream = ostringstream() 1157 if output == randltlgenerator.LTL: 1158 print('Use argument ltl_priorities=STRING to set the following ' 1159 'LTL priorities:\n') 1160 rg.dump_ltl_priorities(dumpstream) 1161 print(dumpstream.str()) 1162 elif output == randltlgenerator.Bool: 1163 print('Use argument boolean_priorities=STRING to set the ' 1164 'following Boolean formula priorities:\n') 1165 rg.dump_bool_priorities(dumpstream) 1166 print(dumpstream.str()) 1167 elif output == randltlgenerator.PSL or output == randltlgenerator.SERE: 1168 if output != randltlgenerator.SERE: 1169 print('Use argument ltl_priorities=STRING to set the ' 1170 'following LTL priorities:\n') 1171 rg.dump_psl_priorities(dumpstream) 1172 print(dumpstream.str()) 1173 print('Use argument sere_priorities=STRING to set the ' 1174 'following SERE priorities:\n') 1175 rg.dump_sere_priorities(dumpstream) 1176 print(dumpstream.str()) 1177 print('Use argument boolean_priorities=STRING to set the ' 1178 'following Boolean formula priorities:\n') 1179 rg.dump_sere_bool_priorities(dumpstream) 1180 print(dumpstream.str()) 1181 else: 1182 sys.stderr.write("internal error: unknown type of output") 1183 return 1184 1185 class _randltliterator: 1186 def __init__(self, rg, n): 1187 self.rg = rg 1188 self.i = 0 1189 self.n = n 1190 1191 def __iter__(self): 1192 return self 1193 1194 def __next__(self): 1195 if self.i == self.n: 1196 raise StopIteration 1197 f = self.rg.next() 1198 if f is None: 1199 sys.stderr.write("Warning: could not generate a new " 1200 "unique formula after {} trials.\n" 1201 .format(randltlgenerator.MAX_TRIALS)) 1202 raise StopIteration 1203 self.i += 1 1204 return f 1205 1206 return formulaiterator(_randltliterator(rg, n)) 1207 1208 1209def simplify(f, **kwargs): 1210 level = kwargs.get('level', None) 1211 if level is not None: 1212 return tl_simplifier(tl_simplifier_options(level)).simplify(f) 1213 1214 basics = kwargs.get('basics', True) 1215 synt_impl = kwargs.get('synt_impl', True) 1216 event_univ = kwargs.get('event_univ', True) 1217 cont_checks = kwargs.get('containment_checks', False) 1218 cont_checks_stronger = kwargs.get('containment_checks_stronger', False) 1219 nenoform_stop_on_boolean = kwargs.get('nenoform_stop_on_boolean', False) 1220 reduce_size_strictly = kwargs.get('reduce_size_strictly', False) 1221 boolean_to_isop = kwargs.get('boolean_to_isop', False) 1222 favor_event_univ = kwargs.get('favor_event_univ', False) 1223 1224 simp_opts = tl_simplifier_options(basics, 1225 synt_impl, 1226 event_univ, 1227 cont_checks, 1228 cont_checks_stronger, 1229 nenoform_stop_on_boolean, 1230 reduce_size_strictly, 1231 boolean_to_isop, 1232 favor_event_univ) 1233 return tl_simplifier(simp_opts).simplify(f) 1234 1235 1236for fun in dir(formula): 1237 if (callable(getattr(formula, fun)) and (fun[:3] == 'is_' or 1238 fun[:4] == 'has_')): 1239 _addfilter(fun) 1240 1241for fun in ['remove_x', 'relabel', 'relabel_bse', 1242 'simplify', 'unabbreviate', 'negative_normal_form', 1243 'mp_class', 'nesting_depth']: 1244 _addmap(fun) 1245 1246 1247# Better interface to the corresponding C++ function. 1248def sat_minimize(aut, acc=None, colored=False, 1249 state_based=False, states=0, 1250 max_states=0, sat_naive=False, sat_langmap=False, 1251 sat_incr=0, sat_incr_steps=0, 1252 display_log=False, return_log=False): 1253 args = '' 1254 if acc is not None: 1255 if type(acc) is not str: 1256 raise ValueError("argument 'acc' should be a string") 1257 args += ',acc="' + acc + '"' 1258 if colored: 1259 args += ',colored' 1260 if states: 1261 if type(states) is not int or states < 0: 1262 raise ValueError("argument 'states' should be a positive integer") 1263 args += ',states=' + str(states) 1264 if max_states: 1265 if type(max_states) is not int or max_states < 0: 1266 raise ValueError("argument 'states' should be a positive integer") 1267 args += ',max-states=' + str(max_states) 1268 if sat_naive: 1269 args += ',sat-naive' 1270 if sat_langmap: 1271 args += ',sat-langmap' 1272 if sat_incr: 1273 args += ',sat-incr=' + str(sat_incr) 1274 args += ',sat-incr-steps=' + str(sat_incr_steps) 1275 from spot.impl import sat_minimize as sm 1276 1277 if display_log or return_log: 1278 import pandas as pd 1279 with tempfile.NamedTemporaryFile(dir='.', suffix='.satlog') as t: 1280 args += ',log="{}"'.format(t.name) 1281 aut = sm(aut, args, state_based) 1282 dfrm = pd.read_csv(t.name, dtype=object) 1283 if display_log: 1284 # old versions of ipython do not import display by default 1285 from IPython.display import display 1286 del dfrm['automaton'] 1287 display(dfrm) 1288 if return_log: 1289 return aut, dfrm 1290 else: 1291 return aut 1292 else: 1293 return sm(aut, args, state_based) 1294 1295 1296def parse_word(word, dic=_bdd_dict): 1297 from spot.impl import parse_word as pw 1298 return pw(word, dic) 1299 1300 1301def bdd_to_formula(b, dic=_bdd_dict): 1302 from spot.impl import bdd_to_formula as bf 1303 return bf(b, dic) 1304 1305 1306def language_containment_checker(dic=_bdd_dict): 1307 from spot.impl import language_containment_checker as c 1308 c.contains = lambda this, a, b: c.contained(this, b, a) 1309 c.are_equivalent = lambda this, a, b: c.equal(this, a, b) 1310 return c(dic) 1311 1312 1313def mp_hierarchy_svg(cl=None): 1314 """ 1315 Return an some string containing an SVG picture of the Manna & 1316 Pnueli hierarchy, highlighting class `cl` if given. 1317 1318 If not None, `cl` should be one of 'TPROGSB'. For convenience, 1319 if `cl` is an instance of `spot.formula`, it is replaced by 1320 `mp_class(cl)`. 1321 1322 """ 1323 if type(cl) == formula: 1324 cl = mp_class(cl) 1325 ch = None 1326 coords = { 1327 'T': '110,35', 1328 'R': '40,80', 1329 'P': '175,80', 1330 'O': '110,140', 1331 'S': '40,160', 1332 'G': '175,160', 1333 'B': '110,198', 1334 } 1335 if cl in coords: 1336 highlight = '''<g transform="translate({})"> 1337 <line x1="-10" y1="-10" x2="10" y2="10" stroke="red" stroke-width="5" /> 1338 <line x1="-10" y1="10" x2="10" y2="-10" stroke="red" stroke-width="5" /> 1339 </g>'''.format(coords[cl]) 1340 else: 1341 highlight = '' 1342 return ''' 1343<svg height="210" width="220" xmlns="http://www.w3.org/2000/svg" version="1.1"> 1344<polygon points="20,0 200,120 200,210 20,210" fill="cyan" opacity=".2" /> 1345<polygon points="20,120 155,210 20,210" fill="cyan" opacity=".2" /> 1346<polygon points="200,0 20,120 20,210 200,210" fill="magenta" opacity=".15" /> 1347<polygon points="200,120 65,210 200,210" fill="magenta" opacity=".15" /> 1348''' + highlight + ''' 1349<g text-anchor="middle" font-size="14"> 1350<text x="110" y="20">Reactivity</text> 1351<text x="60" y="65">Recurrence</text> 1352<text x="160" y="65">Persistence</text> 1353<text x="110" y="125">Obligation</text> 1354<text x="60" y="185">Safety</text> 1355<text x="160" y="185">Guarantee</text> 1356</g> 1357<g font-size="14"> 1358<text text-anchor="begin" transform="rotate(-90,18,210)" x="18" y="210" fill="gray">Monitor</text> 1359<text text-anchor="end" transform="rotate(-90,18,0)" x="18" y="0" fill="gray">Deterministic Büchi</text> 1360<text text-anchor="begin" transform="rotate(-90,214,210)" x="214" y="210" fill="gray">Terminal Büchi</text> 1361<text text-anchor="end" transform="rotate(-90,214,0)" x="214" y="0" fill="gray">Weak Büchi</text> 1362</g> 1363</svg>''' 1364 1365 1366def show_mp_hierarchy(cl): 1367 """ 1368 Return a picture of the Manna & Pnueli hierarchy as an SVG object 1369 in the IPython/Jupyter. 1370 """ 1371 from spot.jupyter import SVG 1372 return SVG(mp_hierarchy_svg(cl)) 1373 1374 1375formula.show_mp_hierarchy = show_mp_hierarchy 1376 1377 1378@_extend(twa_word) 1379class twa_word: 1380 def _repr_latex_(self): 1381 bd = self.get_dict() 1382 res = '$' 1383 for idx, letter in enumerate(self.prefix): 1384 if idx: 1385 res += '; ' 1386 res += bdd_to_formula(letter, bd).to_str('j') 1387 if len(res) > 1: 1388 res += '; ' 1389 res += '\\mathsf{cycle}\\{' 1390 for idx, letter in enumerate(self.cycle): 1391 if idx: 1392 res += '; ' 1393 res += bdd_to_formula(letter, bd).to_str('j') 1394 return res + '\\}$' 1395 1396 def as_svg(self): 1397 """ 1398 Build an SVG picture representing the word as a collection of 1399 signals for each atomic proposition. 1400 """ 1401 # Get the list of atomic proposition used 1402 sup = buddy.bddtrue 1403 for cond in list(self.prefix) + list(self.cycle): 1404 sup = sup & buddy.bdd_support(cond) 1405 ap = [] 1406 while sup != buddy.bddtrue: 1407 a = buddy.bdd_var(sup) 1408 ap.append(a) 1409 sup = buddy.bdd_high(sup) 1410 1411 # Prepare canvas 1412 psize = len(self.prefix) 1413 csize = len(self.cycle) 1414 d = { 1415 'endprefix': 50 * psize, 1416 'endcycle': 50 * (psize + csize), 1417 'w': 50 * (psize + csize * 2), 1418 'height': 50 * len(ap), 1419 'height2': 50 * len(ap) + 10, 1420 'h3': 50 * len(ap) + 12, 1421 'bgcolor': '#f4f4f4', 1422 'bgl': 'stroke="white" stroke-width="4"', 1423 'bgt': 'stroke="white" stroke-width="1"', 1424 'txt': 'text-anchor="start" font-size="20"', 1425 'red': 'stroke="#ff0000" stroke-width="2"', 1426 'sml': 'text-anchor="start" font-size="10"' 1427 } 1428 txt = ''' 1429<svg height="{h3}" width="{w}" xmlns="http://www.w3.org/2000/svg" version="1.1"> 1430<rect x="0" y="0" width="{w}" height="{height}" fill="{bgcolor}"/> 1431<line x1="{endprefix}" y1="0" x2="{endprefix}" y2="{height}" 1432 stroke="white" stroke-width="4"/> 1433<line x1="{endcycle}" y1="0" x2="{endcycle}" y2="{height}" 1434 stroke="white" stroke-width="4"/> 1435'''.format(**d) 1436 1437 # Iterate over all used atomic propositions, and fill each line 1438 l = list(self.prefix) + list(self.cycle) + list(self.cycle) 1439 bd = self.get_dict() 1440 for ypos, a in enumerate(ap): 1441 pa = buddy.bdd_ithvar(a) 1442 na = buddy.bdd_nithvar(a) 1443 name = bdd_format_formula(bd, pa) 1444 # Whether the last state was down (-1), up (1), or unknown (0) 1445 last = 0 1446 txt += ('<line x1="0" y1="{y}" x2="{w}" y2="{y}" {bgl}/>' 1447 .format(y=ypos*50, **d)) 1448 txt += ('<text x="{x}" y="{y}" {txt}>{name}</text>' 1449 .format(x=3, y=ypos*50+30, name=name, **d)) 1450 for xpos, step in enumerate(l): 1451 if buddy.bdd_implies(step, pa): 1452 cur = 1 1453 elif buddy.bdd_implies(step, na): 1454 cur = -1 1455 else: 1456 cur = 0 1457 txt += ('<line x1="{x}" y1="{y1}" x2="{x}" y2="{y2}" {bgt}/>' 1458 .format(x=(xpos+1)*50, y1=ypos*50, y2=ypos*50+50, **d)) 1459 if cur != 0: 1460 if last == -cur: 1461 txt += \ 1462 ('<line x1="{x}" y1="{y1}" x2="{x}" y2="{y2}" {red}/>' 1463 .format(x=xpos*50, y1=ypos*50+5, 1464 y2=ypos*50+45, **d)) 1465 txt += \ 1466 ('<line x1="{x1}" y1="{y}" x2="{x2}" y2="{y}" {red}/>' 1467 .format(x1=xpos*50, x2=(xpos+1)*50, 1468 y=ypos*50+25-20*cur, **d)) 1469 last = cur 1470 if psize > 0: 1471 txt += '<text x="0" y="{height2}" {sml}>prefix</text>'.format(**d) 1472 txt += '''<text x="{endprefix}" y="{height2}" {sml}>cycle</text> 1473<text x="{endcycle}" y="{height2}" {sml}>cycle</text>'''.format(**d) 1474 return txt + '</svg>' 1475 1476 def show(self): 1477 """ 1478 Display the word as an SVG picture of signals. 1479 """ 1480 from spot.jupyter import SVG 1481 return SVG(self.as_svg()) 1482 1483 1484# Make scc_and_mark filter usable as context manager 1485@_extend(scc_and_mark_filter) 1486class scc_and_mark_filter: 1487 def __enter__(self): 1488 return self 1489 1490 def __exit__(self, exc_type, exc_value, traceback): 1491 self.restore_acceptance() 1492 1493 1494def to_parity(aut, options = None, **kwargs): 1495 """Convert aut into a parity acceptance. 1496 1497 This procedure combines multiple strategies to attempt to 1498 produce a small parity automaton. The resulting parity 1499 acceptance is either "max odd" or "max even". 1500 1501 The default optimization options maybe altered by passing either an 1502 instance of to_parity_options object as options argument, or by 1503 passing additional kwargs that will be used to update options. 1504 1505 Note that if you pass both your own options object and kwargs, 1506 options will be updated in place. 1507 """ 1508 if options is None: 1509 # Can't make this a default option, otherwise the default 1510 # instance would be updated by the kwargs. 1511 options = to_parity_options() 1512 if kwargs: 1513 for key,val in to_parity_options.__dict__.items(): 1514 if not key.startswith('_') and key != "thisown" and key in kwargs: 1515 setattr(options, key, kwargs.get(key)) 1516 return impl.to_parity(aut, options) 1517