diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 8b62f86ae..3f0369775 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -860,3 +860,7 @@ def sat_minimize(aut, acc=None, colored=False, args += ',dichotomy'; from spot.impl import sat_minimize as sm return sm(aut, args, state_based) + +def parse_word(word, dic=_bdd_dict): + from spot.impl import parse_word as pw + return pw(word, dic) diff --git a/spot/twaalgos/word.cc b/spot/twaalgos/word.cc index e83df00e0..7a8087153 100644 --- a/spot/twaalgos/word.cc +++ b/spot/twaalgos/word.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -20,10 +20,13 @@ #include #include #include +#include +#include +#include namespace spot { - twa_word::twa_word(const twa_run_ptr run) + twa_word::twa_word(const twa_run_ptr& run) : dict_(run->aut->get_dict()) { for (auto& i: run->prefix) @@ -33,6 +36,11 @@ namespace spot dict_->register_all_variables_of(run->aut, this); } + twa_word::twa_word(const bdd_dict_ptr& dict) + : dict_(dict) + { + } + void twa_word::simplify() { @@ -105,4 +113,143 @@ namespace spot os << '}'; return os; } + + namespace + { + static void word_parse_error(const std::string& word, + size_t i, parse_error_list pel) + { + for (auto& err: pel) + { + err.first.begin.column += i; + err.first.end.column += i; + } + std::ostringstream os; + format_parse_errors(os, word, pel); + throw parse_error(os.str()); + } + + static void word_parse_error(const std::string& word, size_t i, + const std::string& message) + { + if (i == std::string::npos) + i = word.size(); + std::ostringstream s; + s << ">>> " << word << '\n'; + for (auto j = i + 4; j > 0; --j) + s << ' '; + s << '^' << '\n'; + s << message << '\n'; + throw parse_error(s.str()); + } + + static size_t skip_next_formula(const std::string& word, size_t begin) + { + bool quoted = false; + auto size = word.size(); + for (auto j = begin; j < size; ++j) + { + auto c = word[j]; + if (!quoted && (c == ';' || c == '}')) + return j; + if (c == '"') + quoted = !quoted; + else if (quoted && c == '\\') + ++j; + } + if (quoted) + word_parse_error(word, word.size(), "Unclosed string"); + return std::string::npos; + } + } + + twa_word_ptr parse_word(const std::string& word, const bdd_dict_ptr& dict) + { + atomic_prop_set aps; + parse_error_list pel; + tl_simplifier tls(dict); + twa_word_ptr tw = make_twa_word(dict); + size_t i = 0; + auto ind = i; + + auto extract_bdd = + [&](typename twa_word::seq_t& seq) + { + auto sub = word.substr(i, ind - i); + formula f = spot::parse_infix_boolean(sub, pel); + if (!pel.empty()) + word_parse_error(word, i, pel); + atomic_prop_collect(f, &aps); + seq.push_back(tls.as_bdd(f)); + if (word[ind] == '}') + return true; + // Skip blanks after semi-colon + i = word.find_first_not_of(' ', ind + 1); + return false; + }; + + // Parse the prefix part. Can be empty. + while (word.substr(i, 6) != std::string("cycle{")) + { + ind = skip_next_formula(word, i); + if (ind == std::string::npos) + word_parse_error(word, word.size(), + "A twa_word must contain a cycle"); + if (word[ind] == '}') + word_parse_error(word, ind, "Expected ';' delimiter :" + "'}' stands for ending a cycle"); + // Exract formula, convert it to bdd and add it to the prefix sequence + extract_bdd(tw->prefix); + if (i == std::string::npos) + word_parse_error(word, ind + 1, "Missing cycle in formula"); + } + // Consume "cycle{" + i += 6; + while (true) + { + ind = skip_next_formula(word, i); + if (ind == std::string::npos) + word_parse_error(word, word.size(), + "Missing ';' or '}' after formula"); + // Extract formula, convert it to bdd and add it to the cycle sequence + // Break if an '}' is encountered + if (extract_bdd(tw->cycle)) + break; + if (i == std::string::npos) + word_parse_error(word, ind + 1, + "Missing end of cycle character : '}'"); + } + if (ind != word.size() - 1) + word_parse_error(word, ind + 1, "Input should be finished after cycle"); + for (auto ap: aps) + dict->register_proposition(ap, tw.get()); + return tw; + } + + twa_graph_ptr twa_word::as_automaton() const + { + twa_graph_ptr aut = make_twa_graph(dict_); + + aut->prop_weak(true); + aut->prop_deterministic(true); + + size_t i = 0; + aut->new_states(prefix.size() + cycle.size()); + for (auto b: prefix) + { + aut->new_edge(i, i + 1, b); + ++i; + } + size_t j = i; + auto b = cycle.begin(); + auto end = --cycle.end(); + for (; b != end; ++b) + { + aut->new_edge(i, i + 1, *b); + ++i; + } + // Close the loop + aut->new_edge(i, j, *b); + return aut; + } } diff --git a/spot/twaalgos/word.hh b/spot/twaalgos/word.hh index e69706ce3..fa9cdf701 100644 --- a/spot/twaalgos/word.hh +++ b/spot/twaalgos/word.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -28,7 +28,8 @@ namespace spot /// \brief An infinite word stored as a lasso. struct SPOT_API twa_word final { - twa_word(const twa_run_ptr run); + twa_word(const bdd_dict_ptr& dict); + twa_word(const twa_run_ptr& run); ~twa_word() { dict_->unregister_all_my_variables(this); @@ -45,10 +46,26 @@ namespace spot return dict_; } + twa_graph_ptr as_automaton() const; + SPOT_API friend std::ostream& operator<<(std::ostream& os, const twa_word& w); private: bdd_dict_ptr dict_; }; + typedef std::shared_ptr twa_word_ptr; + + inline twa_word_ptr make_twa_word(const bdd_dict_ptr& dict) + { + return std::make_shared(dict); + } + + inline twa_word_ptr make_twa_word(const twa_run_ptr& run) + { + return std::make_shared(run); + } + + SPOT_API + twa_word_ptr parse_word(const std::string& word, const bdd_dict_ptr& dict); } diff --git a/tests/python/word.ipynb b/tests/python/word.ipynb index 1e95f4e6f..04f54e2f4 100644 --- a/tests/python/word.ipynb +++ b/tests/python/word.ipynb @@ -1,7 +1,7 @@ { "metadata": { "name": "", - "signature": "sha256:e975b9a64657f38248c434a89f29b28f0bf90f9c40b7e8afdd7459734cbdcd38" + "signature": "sha256:6461a5fa3f321dac24ae47d88c90f911822e003b658d05d4ef7c102ff64e058e" }, "nbformat": 3, "nbformat_minor": 0, @@ -139,7 +139,7 @@ "\n" ], "text": [ - " *' at 0x7f4f0c2e0810> >" + " *' at 0x7fdd0c5d9330> >" ] } ], @@ -294,6 +294,224 @@ } ], "prompt_number": 7 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(spot.parse_word('a; b; cycle{a&b}'))\n", + "print(spot.parse_word('cycle{a&bb|bac&(aaa|bbb)}'))\n", + "print(spot.parse_word('a; b;b; qiwuei;\"a;b&c;a\" ;cycle{a}'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "a; b; cycle{a & b}\n", + "cycle{(a & bb) | (aaa & bac) | (bac & bbb)}\n", + "a; b; b; qiwuei; \"a;b&c;a\"; cycle{a}\n" + ] + } + ], + "prompt_number": 8 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(spot.parse_word('a; b&!a; b'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "ename": "SyntaxError", + "evalue": "\n>>> a; b&!a; b\n ^\nA twa_word must contain a cycle\n ()", + "output_type": "pyerr", + "traceback": [ + "\u001b[0;36m File \u001b[0;32m\"\"\u001b[0;36m, line \u001b[0;32munknown\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \n>>> a; b&!a; b\n ^\nA twa_word must contain a cycle\n\n" + ] + } + ], + "prompt_number": 9 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(spot.parse_word('a; b; c}'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "ename": "SyntaxError", + "evalue": "\n>>> a; b; c}\n ^\nExpected ';' delimiter :'}' stands for ending a cycle\n ()", + "output_type": "pyerr", + "traceback": [ + "\u001b[0;36m File \u001b[0;32m\"\"\u001b[0;36m, line \u001b[0;32munknown\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \n>>> a; b; c}\n ^\nExpected ';' delimiter :'}' stands for ending a cycle\n\n" + ] + } + ], + "prompt_number": 10 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(spot.parse_word('a; cycle{}'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "ename": "SyntaxError", + "evalue": "\n>>> a; cycle{}\n ^\nempty input\n\n ()", + "output_type": "pyerr", + "traceback": [ + "\u001b[0;36m File \u001b[0;32m\"\"\u001b[0;36m, line \u001b[0;32munknown\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \n>>> a; cycle{}\n ^\nempty input\n\n\n" + ] + } + ], + "prompt_number": 11 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(spot.parse_word('a; cycle{!a}; a'))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "ename": "SyntaxError", + "evalue": "\n>>> a; cycle{!a}; a\n ^\nInput should be finished after cycle\n ()", + "output_type": "pyerr", + "traceback": [ + "\u001b[0;36m File \u001b[0;32m\"\"\u001b[0;36m, line \u001b[0;32munknown\u001b[0m\n\u001b[0;31mSyntaxError\u001b[0m\u001b[0;31m:\u001b[0m \n>>> a; cycle{!a}; a\n ^\nInput should be finished after cycle\n\n" + ] + } + ], + "prompt_number": 12 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "w1 = spot.parse_word('a; !a; cycle{a; !a; a}')" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 13 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "w1.as_automaton()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 14, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7fdd0c5d96c0> >" + ] + } + ], + "prompt_number": 14 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [], + "language": "python", + "metadata": {}, + "outputs": [] } ], "metadata": {}