Commit 2362b9ab authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

python: improve handling of formulas

* src/misc/escape.hh, src/misc/escape.cc (escape_latex): New function.
* src/ltlvisit/tostring.cc: Escape atomic proposition in LaTeX output.
* wrap/python/spot.py: Make it easy to output formulas in different
syntaxes.  Also allow the AST to be shown.
* wrap/python/spot_impl.i: Catch std::runtime_error.
* wrap/python/tests/formulas.ipynb: New file.
* wrap/python/tests/Makefile.am: Add it.
parent a6dbf5cf
......@@ -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())
......
// -*- 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;
......
// -*- 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:
/// <code>& % $ # _ { } ~ ^ \\</code>
SPOT_API std::ostream&
escape_latex(std::ostream& os, const std::string& str);
/// \brief Escape characters <code>"</code>, <code>\\</code>, and
/// <code>\\n</code> in \a str.
SPOT_API std::ostream&
......
# -*- 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)
......@@ -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());
}
}
......
## Copyright (C) 2010, 2012, 2013, 2014 Labortatoire de Recherche et Dveloppement 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),
## dpartement Systmes Rpartis Coopratifs (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 \
......
{
"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": [
"<svg height=\"260pt\" viewBox=\"0.00 0.00 269.00 260.00\" width=\"269pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",