diff --git a/tests/python/acc_cond.ipynb b/tests/python/acc_cond.ipynb index e14b85fda..76580fcdd 100644 --- a/tests/python/acc_cond.ipynb +++ b/tests/python/acc_cond.ipynb @@ -542,7 +542,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The manipulation of `acc_code` objects is quite rudimentary at the moment: they are easy to build, but are harder take appart. In fact we won't attempt to disassemble an `acc_code` object in Python: those things are better done in C++\n", + "The manipulation of `acc_code` objects is quite rudimentary at the moment: they are easy to build, but are harder take appart. In fact we won't attempt to disassemble an `acc_code` object in Python: those things are better done in C++.\n", "\n", "Operators `|`, `|=`, `&`, `&=`, `<<`, and `<<=` can be used with their obvious semantics.\n", "Whenever possible, the inplace versions (`|=`, `&=`, `<<=`) should be prefered, because they create less temporary acceptance conditions." @@ -1501,9 +1501,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.2" + "version": "3.7.3" } }, "nbformat": 4, - "nbformat_minor": 2 + "nbformat_minor": 4 } diff --git a/tests/python/contains.ipynb b/tests/python/contains.ipynb index 626a2ab9d..ca8e65bdc 100644 --- a/tests/python/contains.ipynb +++ b/tests/python/contains.ipynb @@ -310,7 +310,7 @@ "source": [ "# Help for distinguishing languages\n", "\n", - "Assume you have computed two automata, that `are_equivalent(a1, a2)` returns `False`, and you want to know why. (This often occur when debugging some algorithm that produce an automaton that is not equivalent to which it should.) The automaton class has a method called `a1.exclusive_run(a2)` that can help with this task: it returns a run that recognizes a word is is accepted by one of the two automata but not by both. The method `a1.exclusive_run(a2)` will return just a word.\n", + "Assume you have computed two automata, that `are_equivalent(a1, a2)` returns `False`, and you want to know why. (This often occur when debugging some algorithm that produce an automaton that is not equivalent to which it should.) The automaton class has a method called `a1.exclusive_run(a2)` that can help with this task: it returns a run that recognizes a word is is accepted by one of the two automata but not by both. The method `a1.exclusive_word(a2)` will return just a word.\n", "\n", "For instance let's find a word that is exclusive between `aut_f` and `aut_g`. (The adjective *exlusive* is a reference to the *exclusive or* operator: the word belongs to L(aut_f) \"xor\" it belongs to L(aut_g).)" ] @@ -509,5 +509,5 @@ } }, "nbformat": 4, - "nbformat_minor": 2 + "nbformat_minor": 4 } diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index 7f23b1777..d7c2061a2 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -5950,13 +5950,6 @@ "source": [ "spot.decompose_scc(si, 'a2')" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { @@ -5975,9 +5968,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.2" + "version": "3.7.3" } }, "nbformat": 4, - "nbformat_minor": 2 + "nbformat_minor": 4 } diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb index f6277d0f6..026ff0095 100644 --- a/tests/python/games.ipynb +++ b/tests/python/games.ipynb @@ -19,7 +19,7 @@ "\n", "The support for games is currently quite rudimentary, as Spot currently only uses those games in `ltlsynt`.\n", "\n", - "In essence, agame is just an ω-automaton with a property named `state-player` that stores the player owning each state. The players are named 0 and 1. The player owning a state can decide what the next transition from this state should be. The goal for player 1 is to force the play to be infinite and to satisfy the acceptance condition of the automaton, while the goal for player 0 is to prevent it by either forcing a finite play, or forcing an infinite play that does not satisfy the acceptance condition.\n", + "In essence, a game is just an ω-automaton with a property named `state-player` that stores the player owning each state. The players are named 0 and 1. The player owning a state can decide what the next transition from this state should be. The goal for player 1 is to force the play to be infinite and to satisfy the acceptance condition of the automaton, while the goal for player 0 is to prevent it by either forcing a finite play, or forcing an infinite play that does not satisfy the acceptance condition.\n", "\n", "The support is currently restricted to games that use:\n", "- `t` acceptance: all infinite run are accepting, and player 0 can only win if it manages to force a finite play (this requires reaching states without successors).\n", @@ -218,7 +218,7 @@ " (6, 7),\n", " (7, 6), (7, 8),\n", " (8, 5)):\n", - " game.new_edge(s, d, bddtrue)\n", + " game.new_edge(s, d, bddtrue)\n", "spot.set_state_players(game, [True, False, True, False, True, True, True, False, False])\n", "game.show('.g') # Use \"g\" to hide the irrelevant edge labels." ] @@ -678,9 +678,7 @@ { "cell_type": "code", "execution_count": 8, - "metadata": { - "scrolled": false - }, + "metadata": {}, "outputs": [ { "data": { @@ -1326,7 +1324,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.2" + "version": "3.7.3" } }, "nbformat": 4, diff --git a/tests/python/randltl.ipynb b/tests/python/randltl.ipynb index 7209275ab..4fcde84e9 100644 --- a/tests/python/randltl.ipynb +++ b/tests/python/randltl.ipynb @@ -477,7 +477,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "most boolean functions found in the class formula can be used to filter the random formula generator like this:" + "most Boolean functions found in the class formula can be used to filter the random formula generator like this:" ] }, { @@ -541,7 +541,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Since the boolean filters and mapping functions return an iterator of the same type, these operations can be chained like this:" + "Since the Boolean filters and mapping functions return an iterator of the same type, these operations can be chained like this:" ] }, { @@ -613,9 +613,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.4+" + "version": "3.7.3" } }, "nbformat": 4, - "nbformat_minor": 2 + "nbformat_minor": 4 } diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb index ce1e98e14..5a9d3f29e 100644 --- a/tests/python/synthesis.ipynb +++ b/tests/python/synthesis.ipynb @@ -3619,7 +3619,7 @@ "\n", "Note that we do not support the full [AIGER syntax](http://fmv.jku.at/aiger/FORMAT.aiger). Our restrictions corresponds to the conventions used in the type of AIGER file we output:\n", "- Input variables start at index 2 and are consecutively numbered.\n", - "- Latch variables start at index (1 + #inputs) * 2 and are consecutively numbered.\n", + "- Latch variables start at index (1 + #inputs) × 2 and are consecutively numbered.\n", "- If some inputs or outputs are named in comments, all of them have to be named.\n", "- Gate number $n$ can only connect to latches, inputs, or previously defined gates ($