diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc
index 759e53492..21e737300 100644
--- a/src/ltlvisit/tostring.cc
+++ b/src/ltlvisit/tostring.cc
@@ -30,7 +30,7 @@
#include "lunabbrev.hh"
#include "wmunabbrev.hh"
#include "tostring.hh"
-
+#include "misc/escape.hh"
namespace spot
{
@@ -416,7 +416,9 @@ namespace spot
{
// Spin 6 supports atomic propositions such as (a == 0)
// as long as they are enclosed in parentheses.
- if (kw_ != spin_kw)
+ if (kw_ == sclatex_kw || kw_ == sclatex_kw)
+ escape_latex(os_ << "``\\mathit{", str) << "\\textrm{''}}";
+ else if (kw_ != spin_kw)
os_ << '"' << str << '"';
else if (!full_parent_)
os_ << '(' << str << ')';
@@ -431,11 +433,11 @@ namespace spot
while (str[s - 1] >= '0' && str[s - 1] <= '9')
{
--s;
- assert(s != 0); // bare words cannot start with letters
+ assert(s != 0); // bare words cannot start with digits
}
if (s > 1)
os_ << "\\mathit{";
- os_ << str.substr(0, s);
+ escape_latex(os_, str.substr(0, s));
if (s > 1)
os_ << '}';
if (s != str.size())
diff --git a/src/misc/escape.cc b/src/misc/escape.cc
index 921addcfc..e9ba8dd3c 100644
--- a/src/misc/escape.cc
+++ b/src/misc/escape.cc
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE)
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -34,14 +34,44 @@ namespace spot
std::ostream&
escape_rfc4180(std::ostream& os, const std::string& str)
{
- for (std::string::const_iterator i = str.begin(); i != str.end(); ++i)
- switch (*i)
+ for (auto i: str)
+ switch (i)
{
case '"':
os << "\"\"";
break;
default:
- os << *i;
+ os << i;
+ break;
+ }
+ return os;
+ }
+
+ std::ostream&
+ escape_latex(std::ostream& os, const std::string& str)
+ {
+ for (auto i: str)
+ switch (i)
+ {
+ case '~':
+ os << "\\textasciitilde";
+ break;
+ case '^':
+ os << "\\textasciicircum";
+ break;
+ case '\\':
+ os << "\\textbackslash";
+ break;
+ case '&':
+ case '%':
+ case '$':
+ case '#':
+ case '_':
+ case '{':
+ case '}':
+ os << '\\';
+ default:
+ os << i;
break;
}
return os;
@@ -50,8 +80,8 @@ namespace spot
std::ostream&
escape_str(std::ostream& os, const std::string& str)
{
- for (std::string::const_iterator i = str.begin(); i != str.end(); ++i)
- switch (*i)
+ for (auto i: str)
+ switch (i)
{
case '\\':
os << "\\\\";
@@ -63,7 +93,7 @@ namespace spot
os << "\\n";
break;
default:
- os << *i;
+ os << i;
break;
}
return os;
diff --git a/src/misc/escape.hh b/src/misc/escape.hh
index 37f086f29..3b1bff613 100644
--- a/src/misc/escape.hh
+++ b/src/misc/escape.hh
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+// Copyright (C) 2011, 2012, 2013, 2015 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -39,6 +39,13 @@ namespace spot
SPOT_API std::ostream&
escape_rfc4180(std::ostream& os, const std::string& str);
+ /// \brief Escape special LaTeX characters.
+ ///
+ /// The following characters are rewritten:
+ /// & % $ # _ { } ~ ^ \\
+ SPOT_API std::ostream&
+ escape_latex(std::ostream& os, const std::string& str);
+
/// \brief Escape characters ", \\, and
/// \\n in \a str.
SPOT_API std::ostream&
diff --git a/wrap/python/spot.py b/wrap/python/spot.py
index 92e411383..535d367ef 100644
--- a/wrap/python/spot.py
+++ b/wrap/python/spot.py
@@ -1,5 +1,5 @@
# -*- coding: utf-8 -*-
-# Copyright (C) 2014 Laboratoire de
+# Copyright (C) 2014, 2015 Laboratoire de
# Recherche et Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@@ -23,27 +23,59 @@ import sys
_bdd_dict = make_bdd_dict()
-def render_automaton_as_svg(a):
- dotsrc = ostringstream()
- dotty_reachable(dotsrc, a)
+def _ostream_to_svg(ostr):
dotty = subprocess.Popen(['dot', '-Tsvg'],
stdin=subprocess.PIPE,
stdout=subprocess.PIPE)
- dotty.stdin.write(dotsrc.str().encode('utf-8'))
+ dotty.stdin.write(ostr.str().encode('utf-8'))
res = dotty.communicate()
return res[0].decode('utf-8')
-tgba._repr_svg_ = render_automaton_as_svg
+def _render_automaton_as_svg(a):
+ ostr = ostringstream()
+ dotty_reachable(ostr, a)
+ return _ostream_to_svg(ostr)
-def formula_str_ctor(self, str):
+tgba._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 _formula_str_ctor(self, str):
self.this = parse_formula(str)
-formula.__init__ = formula_str_ctor
+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)
-def tgba_str_ctor(self, str):
+formula.__init__ = _formula_str_ctor
+formula.to_str = _formula_to_str
+formula.show_ast = _render_formula_as_svg
+
+def _tgba_str_ctor(self, str):
self.this = ltl_to_tgba_fm(parse_formula(str), _bdd_dict)
-tgba.__init__ = tgba_str_ctor
+tgba.__init__ = _tgba_str_ctor
# Wrapper around a formula iterator to which we add some methods of formula
# (using _addfilter and _addmap), so that we can write things like
@@ -211,17 +243,22 @@ def simplify(f, **kwargs):
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)
-
+ 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_':
+ 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']:
+ 'simplify', 'unabbreviate_ltl']:
_addmap(fun)
diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i
index 5a9908d4d..f1b0ea01b 100644
--- a/wrap/python/spot_impl.i
+++ b/wrap/python/spot_impl.i
@@ -190,9 +190,11 @@ using namespace spot;
}
catch (const std::invalid_argument& e)
{
- std::string er("\n");
- er += e.what();
- SWIG_exception(SWIG_ValueError, er.c_str());
+ SWIG_exception(SWIG_ValueError, e.what());
+ }
+ catch (const std::runtime_error& e)
+ {
+ SWIG_exception(SWIG_RuntimeError, e.what());
}
}
diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am
index 1f28a8b45..518866fc4 100644
--- a/wrap/python/tests/Makefile.am
+++ b/wrap/python/tests/Makefile.am
@@ -1,7 +1,8 @@
-## Copyright (C) 2010, 2012, 2013, 2014 Labortatoire de Recherche et Développement de
-## l'EPITA.
+## -*- coding: utf-8 -*-
+## Copyright (C) 2010, 2012, 2013, 2014, 2015 Labortatoire de
+## Recherche et Développement de l'EPITA.
## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
-## département Systèmes Répartis Coopératifs (SRC), Université Pierre
+## département Systèmes Répartis Coopératifs (SRC), Université Pierre
## et Marie Curie.
##
## This file is part of Spot, a model checking library.
@@ -32,6 +33,7 @@ check_SCRIPTS = run
TESTS = \
alarm.py \
bddnqueen.py \
+ formulas.ipynb \
implies.py \
interdep.py \
ltl2tgba.test \
diff --git a/wrap/python/tests/formulas.ipynb b/wrap/python/tests/formulas.ipynb
new file mode 100644
index 000000000..439874591
--- /dev/null
+++ b/wrap/python/tests/formulas.ipynb
@@ -0,0 +1,552 @@
+{
+ "metadata": {
+ "name": "",
+ "signature": "sha256:c5ce337080296dc7af1d530e86502099bdfb3f039b96f749f38390b8d5ade44b"
+ },
+ "nbformat": 3,
+ "nbformat_minor": 0,
+ "worksheets": [
+ {
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Handling LTL and PSL formulas\n",
+ "============================="
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "import spot"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [],
+ "prompt_number": 1
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "For interactive use, formulas can be entered as text strings and passed to the `spot.formula` constructor."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f = spot.formula('p1 U p2 R (p3 & !p4)')\n",
+ "f"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "latex": [
+ "$p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))$"
+ ],
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 2,
+ "text": [
+ "p1 U (p2 R (p3 & !p4))"
+ ]
+ }
+ ],
+ "prompt_number": 2
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "g = spot.formula('{a;b*;c[+]}<>->GFb'); g"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "latex": [
+ "$\\{a \\mathbin{\\mathsf{;}} b^{\\star} \\mathbin{\\mathsf{;}} c^+\\}\\mathrel{\\Diamond\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathsf{G} \\mathsf{F} b$"
+ ],
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 3,
+ "text": [
+ "{a;b[*];c[+]}<>-> GFb"
+ ]
+ }
+ ],
+ "prompt_number": 3
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "By default the parser recognizes an infix syntax, but when this fails, it tries to read the formula with the [LBT](http://www.tcs.hut.fi/Software/maria/tools/lbt/) syntax:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "h = spot.formula('& | a b c'); h"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "latex": [
+ "$c \\land (a \\lor b)$"
+ ],
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 4,
+ "text": [
+ "c & (a | b)"
+ ]
+ }
+ ],
+ "prompt_number": 4
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "By default, a formula object is presented using mathjax as above.\n",
+ "When a formula is converted to string you get Spot's syntax by default:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "str(f)"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 5,
+ "text": [
+ "'p1 U (p2 R (p3 & !p4))'"
+ ]
+ }
+ ],
+ "prompt_number": 5
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "If you prefer to print the string in another syntax, you may use the `to_str()` method, with an argument that indicates the output format to use. The `latex` format assumes that you will the define macros such as `\\U`, `\\R` to render all operators as you wish. On the otherhand, the `sclatex` (with `sc` for self-contained) format hard-codes the rendering of each of those operators: this is typically the output that is used to render formulas using MathJax in a notebook. "
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "for i in ['spot', 'spin', 'lbt', 'wring', 'utf8', 'latex', 'sclatex']:\n",
+ " print(\"%-10s%s\" % (i, f.to_str(i)))"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "output_type": "stream",
+ "stream": "stdout",
+ "text": [
+ "spot p1 U (p2 R (p3 & !p4))\n",
+ "spin p1 U (p2 V (p3 && !p4))\n",
+ "lbt U p1 V p2 & p3 ! p4\n",
+ "wring (p1=1) U ((p2=1) R ((p3=1) * (p4=0)))\n",
+ "utf8 p1 U (p2 R (p3\u2227\u00acp4))\n",
+ "latex p_{1} \\U (p_{2} \\R (p_{3} \\land \\lnot p_{4}))\n",
+ "sclatex p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))\n"
+ ]
+ }
+ ],
+ "prompt_number": 6
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "A `spot.formula` object has a number of built-in predicates whose value have been computed when the formula was constructed. For instance you can check whether a formula is in negative normal form using `is_in_nenoform()`, and you can make sure it is an LTL formula (i.e. not a PSL formula) using `is_ltl_formula()`:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f.is_in_nenoform() and f.is_ltl_formula()"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 7,
+ "text": [
+ "True"
+ ]
+ }
+ ],
+ "prompt_number": 7
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "g.is_ltl_formula()"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 8,
+ "text": [
+ "False"
+ ]
+ }
+ ],
+ "prompt_number": 8
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Similarly, `is_syntactic_stutter_invariant()` tells wether the structure of the formula guarranties it to be stutter invariant. For LTL formula, this means the `X` operator should not be used. For PSL formula, this function capture all formulas built using the [siPSL grammar](http://www.daxc.de/eth/paper/09atva.pdf)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f.is_syntactic_stutter_invariant()"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 9,
+ "text": [
+ "True"
+ ]
+ }
+ ],
+ "prompt_number": 9
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "spot.formula('{a[*];b}<>->c').is_syntactic_stutter_invariant()"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 10,
+ "text": [
+ "False"
+ ]
+ }
+ ],
+ "prompt_number": 10
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "spot.formula('{a[+];b[*]}<>->d').is_syntactic_stutter_invariant()"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 11,
+ "text": [
+ "True"
+ ]
+ }
+ ],
+ "prompt_number": 11
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "`spot.relabel` renames the atomic propositions that occur in a formula, using either letters, or numbered propositions:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "gf = spot.formula('(GF_foo_) && \"a > b\" && \"proc[2]@init\"'); gf"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "latex": [
+ "$``\\mathit{a > b\\textrm{''}} \\land ``\\mathit{proc[2]@init\\textrm{''}} \\land \\mathsf{G} \\mathsf{F} \\mathit{\\_foo\\_}$"
+ ],
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 12,
+ "text": [
+ "\"a > b\" & \"proc[2]@init\" & GF_foo_"
+ ]
+ }
+ ],
+ "prompt_number": 12
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "spot.relabel(gf, spot.Abc)"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "latex": [
+ "$a \\land b \\land \\mathsf{G} \\mathsf{F} c$"
+ ],
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 13,
+ "text": [
+ "a & b & GFc"
+ ]
+ }
+ ],
+ "prompt_number": 13
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "spot.relabel(gf, spot.Pnn)"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "latex": [
+ "$p_{0} \\land p_{1} \\land \\mathsf{G} \\mathsf{F} p_{2}$"
+ ],
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 14,
+ "text": [
+ "p0 & p1 & GFp2"
+ ]
+ }
+ ],
+ "prompt_number": 14
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The AST of any formula can be displayed with `show_ast()`. Despite the name, this is not a tree but a DAG, because identical subtrees are merged. Binary operators have their left and right operands denoted with `L` and `R`, while non-commutative n-ary operators have their operands numbered."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "print(g); g.show_ast()"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "output_type": "stream",
+ "stream": "stdout",
+ "text": [
+ "{a;b[*];c[+]}<>-> GFb\n"
+ ]
+ },
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 15,
+ "svg": [
+ ""
+ ],
+ "text": [
+ ""
+ ]
+ }
+ ],
+ "prompt_number": 15
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f = spot.formula('F(a & X(!a & b))'); f"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "latex": [
+ "$\\mathsf{F} (a \\land \\mathsf{X} (\\lnot a \\land b))$"
+ ],
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 16,
+ "text": [
+ "F(a & X(!a & b))"
+ ]
+ }
+ ],
+ "prompt_number": 16
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "spot.remove_x(f)"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "latex": [
+ "$\\mathsf{F} (a \\land ((a \\land (a \\mathbin{\\mathsf{U}} (\\lnot a \\land b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} \\lnot a) \\lor (b \\mathbin{\\mathsf{U}} \\lnot a))) \\lor (\\lnot a \\land (\\lnot a \\mathbin{\\mathsf{U}} (a \\land \\lnot a \\land b)) \\land ((\\lnot b \\mathbin{\\mathsf{U}} a) \\lor (b \\mathbin{\\mathsf{U}} a))) \\lor (b \\land (b \\mathbin{\\mathsf{U}} (\\lnot a \\land b \\land \\lnot b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} \\lnot b) \\lor (a \\mathbin{\\mathsf{U}} \\lnot b))) \\lor (\\lnot b \\land (\\lnot b \\mathbin{\\mathsf{U}} (\\lnot a \\land b)) \\land ((\\lnot a \\mathbin{\\mathsf{U}} b) \\lor (a \\mathbin{\\mathsf{U}} b))) \\lor (\\lnot a \\land b \\land (\\mathsf{G} \\lnot a \\lor \\mathsf{G} a) \\land (\\mathsf{G} \\lnot b \\lor \\mathsf{G} b))))$"
+ ],
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 17,
+ "text": [
+ "F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b))) | (!a & b & (G!a | Ga) & (G!b | Gb))))"
+ ]
+ }
+ ],
+ "prompt_number": 17
+ }
+ ],
+ "metadata": {}
+ }
+ ]
+}
\ No newline at end of file