{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# Documentation for Spot's randltl Python binding" ] }, { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ "import spot" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Basic usage" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Generate random formulas from specified atomic propositions:" ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "0\n", "0 R b\n", "F(XG(F!b M Fb) W (b R a))\n" ] } ], "source": [ "f = spot.randltl(['a', 'b', 'c'])\n", "for i in range(3):\n", " print(next(f))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Generate random formulas using 3 atomic propositions:" ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "0\n", "0 R p1\n", "F(XG(F!p1 M Fp1) W (p1 R p0))\n" ] } ], "source": [ "f = spot.randltl(3)\n", "for i in range(3):\n", " print(next(f))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "By default, there is no limit to the number of formulas generated.
\n", "To specify a number of formulas:" ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "0\n", "0 R p1\n", "F(XG(F!p1 M Fp1) W (p1 R p0))\n", "F(p0 R !p2)\n" ] } ], "source": [ "f = spot.randltl(3, 4)\n", "for formula in f:\n", " print(formula)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Keyword arguments" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## seed" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Seed for the pseudo random number generator (default: 0)." ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "G(p1 U Gp0)\n" ] } ], "source": [ "f = spot.randltl(3, seed=11)\n", "print(next(f))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### output" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Type of formulas to output: 'ltl', 'psl', 'bool' or 'sere' (default: 'ltl')." ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "{{1 | [*0]}[:*] & [*2]}\n" ] } ], "source": [ "f = spot.randltl(3, output='psl', seed=26)\n", "print(next(f))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### allow_dups" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Allow duplicate formulas (default: False)." ] }, { "cell_type": "code", "execution_count": 7, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "0\n", "0\n", "Fp0\n" ] } ], "source": [ "f = spot.randltl(1, allow_dups=True)\n", "print(next(f))\n", "print(next(f))\n", "print(next(f))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### tree_size" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Tree size of the formulas generated, before mandatory simplifications (default: 15)." ] }, { "cell_type": "code", "execution_count": 8, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "G(((p0 U !Xp1) M Gp1) U Gp0)\n" ] } ], "source": [ "f = spot.randltl(3, tree_size=30, seed=11)\n", "print(next(f))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "A range can be specified as a tuple:" ] }, { "cell_type": "code", "execution_count": 9, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "X!(Gp1 M p2) R (!p2 M Xp1)\n", "F(G(F(Gp0 R (1 U Fp2)) M (p2 -> Gp0)) M F((p0 | Fp0) W Gp2))\n" ] } ], "source": [ "f = spot.randltl(3, tree_size=(1, 40))\n", "print(next(f))\n", "print(next(f))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### boolean_priorities, ltl_priorities, sere_priorities, dump_priorities" ] }, { "cell_type": "code", "execution_count": 10, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "0\n", "!p2 & (p1 <-> p2)\n", "p2\n", "p0 & ((p1 & p2) <-> !(!p0 & p1 & p2))\n", "1\n" ] } ], "source": [ "f = spot.randltl(3, output='bool', boolean_priorities='and=10,or=0')\n", "for i in range(5):\n", " print(next(f))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "To see which operators are available along with their default priorities:" ] }, { "cell_type": "code", "execution_count": 11, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Use argument ltl_priorities=STRING to set the following LTL priorities:\n", "\n", "ap\t3\n", "false\t1\n", "true\t1\n", "not\t1\n", "F\t1\n", "G\t1\n", "X\t1\n", "Closure\t1\n", "equiv\t1\n", "implies\t1\n", "xor\t1\n", "R\t1\n", "U\t1\n", "W\t1\n", "M\t1\n", "and\t1\n", "or\t1\n", "EConcat\t1\n", "UConcat\t1\n", "\n", "Use argument sere_priorities=STRING to set the following SERE priorities:\n", "\n", "ap\t3\n", "false\t1\n", "true\t1\n", "not\t1\n", "F\t1\n", "G\t1\n", "X\t1\n", "Closure\t1\n", "equiv\t1\n", "implies\t1\n", "xor\t1\n", "R\t1\n", "U\t1\n", "W\t1\n", "M\t1\n", "and\t1\n", "or\t1\n", "EConcat\t1\n", "UConcat\t1\n", "eword\t1\n", "boolform\t1\n", "star\t1\n", "star_b\t1\n", "fstar\t1\n", "fstar_b\t1\n", "first_match\t1\n", "and\t1\n", "andNLM\t1\n", "or\t1\n", "concat\t1\n", "fusion\t1\n", "\n", "Use argument boolean_priorities=STRING to set the following Boolean formula priorities:\n", "\n", "ap\t3\n", "false\t1\n", "true\t1\n", "not\t1\n", "F\t1\n", "G\t1\n", "X\t1\n", "Closure\t1\n", "equiv\t1\n", "implies\t1\n", "xor\t1\n", "R\t1\n", "U\t1\n", "W\t1\n", "M\t1\n", "and\t1\n", "or\t1\n", "EConcat\t1\n", "UConcat\t1\n", "eword\t1\n", "boolform\t1\n", "star\t1\n", "star_b\t1\n", "fstar\t1\n", "fstar_b\t1\n", "first_match\t1\n", "and\t1\n", "andNLM\t1\n", "or\t1\n", "concat\t1\n", "fusion\t1\n", "ap\t3\n", "false\t1\n", "true\t1\n", "not\t1\n", "equiv\t1\n", "implies\t1\n", "xor\t1\n", "and\t1\n", "or\t1\n", "\n" ] } ], "source": [ "spot.randltl(3, output='psl', dump_priorities=True)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### simplify" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "0 No rewriting
\n", "1 basic rewritings and eventual/universal rules
\n", "2 additional syntactic implication rules
\n", "3 better implications using containment
\n", "default: 3" ] }, { "cell_type": "code", "execution_count": 12, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "G!(!p1 & (Xp2 | F(p0 R Xp2)))\n", "G(p1 | (X!p2 & G(!p0 U X!p2)))\n" ] } ], "source": [ "f = spot.randltl(3, simplify=0, seed=5)\n", "print(next(f))\n", "f = spot.randltl(3, simplify=3, seed=5)\n", "print(next(f))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Filters and maps" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "most boolean functions found in the class formula can be used to filter the random formula generator like this:" ] }, { "cell_type": "code", "execution_count": 13, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "0\n", "0 R p2\n", "F(p0 R !p1)\n", "G(p0 | Fp2) W (FGp2 R !p2)\n", "(p2 R G!p1) | G(p2 U !p0)\n", "(p2 W p0) U p2\n", "F!G(!Gp1 W p1)\n", "G!p1 & (!((p2 & Fp1) M p1) U p1)\n" ] } ], "source": [ "f = spot.randltl(3, 20).is_syntactic_stutter_invariant()\n", "for formula in f:\n", " print(formula)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "likewise, functions from formula to formula can be applied to map the iterator:" ] }, { "cell_type": "code", "execution_count": 14, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "0\n", "!(F!p1 M 1)\n", "(Gp0 | Fp1) M 1\n", "F!(!p1 <-> FGp1)\n", "Gp1 U (p1 U GFp1)\n", "(!p1 U p1) U ((p0 & (p0 U (!p0 & (!p0 -> Fp1))) & ((!p1 U !p0) | (p1 U !p0))) | (!p0 & (!p0 U (p0 & (!p0 -> Fp1))) & ((!p1 U p0) | (p1 U p0))) | (p1 & (p1 U (!p1 & (!p0 -> Fp1))) & ((!p0 U !p1) | (p0 U !p1))) | (!p1 & (!p1 U (p1 & (!p0 -> Fp1))) & ((!p0 U p1) | (p0 U p1))) | ((!p0 -> Fp1) & (Gp0 | G!p0) & (Gp1 | G!p1)))\n" ] } ], "source": [ "f = spot.randltl(2, 6).remove_x()\n", "for formula in f:\n", " print(formula)" ] }, { "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:" ] }, { "cell_type": "code", "execution_count": 15, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "0\n", "Ga\n", "F(a R !b)\n", "G(a | Fb) | (FGb R !b)\n", "G!b | G(a U !c)\n", "b U a\n", "0\n", "0\n" ] } ], "source": [ "f = spot.randltl(3, 20).is_syntactic_stutter_invariant().relabel(spot.Abc).simplify()\n", "for formula in f:\n", " print(formula)" ] }, { "cell_type": "code", "execution_count": 16, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "0\n", "!(1 U !p1)\n", "1 U ((p0 U ((p0 & p1) | !(1 U !p0))) | !(1 U !((1 U !p1) & (1 U p1))))\n", "1 U (!p2 U ((p0 & !p2) | !(1 U p2)))\n", "(!p1 U ((!p1 & (1 U !(1 U !p1))) | !(1 U p1))) | !(1 U !(p0 | (1 U p1)))\n", "X(p2 & X(p2 U (!p0 | !(1 U !p2))))\n", "(1 U p2) | (X(!p2 | !(1 U !p2)) U (1 U (!p1 & (1 U p2))))\n", "XX!(1 U !((X!p1 U (!p2 U (!p0 & !p2))) | X!(1 U !p0)))\n", "XX(1 U (p1 U ((p0 & p1) | !(1 U !p1))))\n", "p2 & Xp0\n" ] } ], "source": [ "for formula in spot.randltl(3, 10).simplify().unabbreviate(\"WMGFR\"): print(formula)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] } ], "metadata": { "kernelspec": { "display_name": "Python 3", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.7.3" } }, "nbformat": 4, "nbformat_minor": 2 }