From c8b8ac60be15aa6d4a00591d5deebd3a053946fb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 22 Aug 2024 17:04:48 +0200 Subject: [PATCH] bin: new ltlmix tool Fixes #400. * spot/tl/randomltl.cc, spot/tl/randomltl.hh: Adjust to accept a set of formula to replace the atomic propositions. * bin/ltlmix.cc: New file. * bin/Makefile.am: Add it. * bin/man/ltlmix.x: New file. * bin/man/Makefile.am: Add it. * doc/org/ltlmix.org: New file. * doc/Makefile.am: Add it. * bin/man/genltl.x, bin/man/randltl.x, bin/man/spot.x, bin/spot.cc, doc/org/arch.tex, doc/org/concepts.org, doc/org/tools.org, NEWS: Mention ltlmix. * tests/core/ltlmix.test: New file. * tests/Makefile.am: Add it. --- NEWS | 7 +- bin/Makefile.am | 2 + bin/ltlmix.cc | 302 ++++++++++++++++++++++++++++++++++ bin/man/Makefile.am | 4 + bin/man/genltl.x | 1 + bin/man/ltlmix.x | 7 + bin/man/randltl.x | 1 + bin/man/spot.x | 1 + bin/spot.cc | 2 + doc/Makefile.am | 1 + doc/org/arch.tex | 29 ++-- doc/org/concepts.org | 2 +- doc/org/ltlmix.org | 365 +++++++++++++++++++++++++++++++++++++++++ doc/org/tools.org | 2 + spot/tl/randomltl.cc | 122 +++++++++++--- spot/tl/randomltl.hh | 140 ++++++++++------ tests/Makefile.am | 1 + tests/core/ltlmix.test | 93 +++++++++++ 18 files changed, 995 insertions(+), 87 deletions(-) create mode 100644 bin/ltlmix.cc create mode 100644 bin/man/ltlmix.x create mode 100644 doc/org/ltlmix.org create mode 100755 tests/core/ltlmix.test diff --git a/NEWS b/NEWS index cd7c00763..178ba5327 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,9 @@ New in spot 2.12.0.dev (not yet released) Command-line tools: + - ltlmix is a new tool that generate formulas by combining existing + ones. See https://spot.lre.epita.fr/ltlmix.html for examples. + - autfilt learned --restrict-dead-end-edges, to restricts labels of edges leading to dead-ends. See the description of restrict_dead_end_edges_here() below. @@ -38,8 +41,8 @@ New in spot 2.12.0.dev (not yet released) Bug fixes: - - Generating random formula without any unary opertors would very - often create formulas much smaller than asked. + - Generating random formulas without any unary opertor would very + often create formulas much smaller than specified. New in spot 2.12 (2024-05-16) diff --git a/bin/Makefile.am b/bin/Makefile.am index 78d189dc9..b665d859c 100644 --- a/bin/Makefile.am +++ b/bin/Makefile.am @@ -69,6 +69,7 @@ bin_PROGRAMS = \ ltldo \ ltlfilt \ ltlgrind \ + ltlmix \ ltlsynt \ randaut \ randltl @@ -92,6 +93,7 @@ ltl2tgta_SOURCES = ltl2tgta.cc ltlcross_SOURCES = ltlcross.cc ltlgrind_SOURCES = ltlgrind.cc ltldo_SOURCES = ltldo.cc +ltlmix_SOURCES = ltlmix.cc ltlsynt_SOURCES = ltlsynt.cc dstar2tgba_SOURCES = dstar2tgba.cc spot_x_SOURCES = spot-x.cc diff --git a/bin/ltlmix.cc b/bin/ltlmix.cc new file mode 100644 index 000000000..9e6ada1c1 --- /dev/null +++ b/bin/ltlmix.cc @@ -0,0 +1,302 @@ +// -*- coding: utf-8 -*- +// Copyright (C) by the Spot authors, see the AUTHORS file for details. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + + +#include "common_sys.hh" +#include +#include "error.h" + +#include "common_setup.hh" +#include "common_finput.hh" +#include "common_output.hh" +#include "common_conv.hh" +#include "common_cout.hh" +#include "common_range.hh" + +#include +#include +#include + +enum { + OPT_BOOLEAN_PRIORITIES = 256, + OPT_DUMP_PRIORITIES, + OPT_DUPS, + OPT_LTL_PRIORITIES, + OPT_SEED, + OPT_TREE_SIZE, +}; + +static const char * argp_program_doc = + "Combine formulas taken randomly from an input set.\n\n\ +The input set is specified using FILENAME, -F FILENAME, or -f formula.\n\ +By default this generates a Boolean pattern of size 5, for instance\n\ +\"(φ₁ & φ₂) | φ₃\", where each φᵢ is randomly taken from the input set.\n\ +The size and nature of the pattern can be changed using generation\n\ +parameters. Additionally, it is possible to rename the atomic propositions\n\ +in each φᵢ using -A or -P.\v\ +Example:\n\ +\n\ +Generates 10 random Boolean combinations of terms of the form GFa, with\n\ +'a' picked from a set of 5 atomic propositions:\n\ + % ltlmix -f GFa -n10 -A5\n\ +\n\ +Build a single LTL formula over subformulas taken randomly from the list of\n\ +55 patterns by Dwyer et al., using a choice of 10 atomic propositions to\n\ +relabel subformulas:\n\ + % genltl --dac | ltlmix -L -A10\n\ +\n\ +Build 5 random positive Boolean combination of GFa and GFb:\n" + // next line is in its own double-quote to please sanity.test + " % ltlmix -f GFa -f GFb --boolean-prio=not=0,xor=0,implies=0,equiv=0 -n5"; + +static const argp_option options[] = { + // Keep this alphabetically sorted (expect for aliases). + /**************************************************/ + { nullptr, 0, nullptr, 0, "Generation parameters:", 2 }, + { "ap-count", 'A', "N", 0, + "rename the atomic propositions in each selected formula by drawing " + "randomly from N atomic propositions (the rewriting is bijective " + "if N is larger than the original set)", 0 }, + { "polarized-ap", 'P', "N", 0, + "similar to -A N, but randomize the polarity of the new atomic " + "proposition", 0 }, + { "boolean", 'B', nullptr, 0, + "generate Boolean combination of formulas (default)", 0 }, + { "allow-dups", OPT_DUPS, nullptr, 0, + "allow duplicate formulas to be output", 0 }, + { "ltl", 'L', nullptr, 0, "generate LTL combinations of subformulas", 0 }, + { "formulas", 'n', "INT", 0, + "number of formulas to generate (default: 1);\n" + "use a negative value for unbounded generation", 0 }, + { "seed", OPT_SEED, "INT", 0, + "seed for the random number generator (default: 0)", 0 }, + { "tree-size", OPT_TREE_SIZE, "RANGE", 0, + "tree size of main pattern generated (default: 5);\n" + "input formulas count as size 1.", 0 }, + /**************************************************/ + { nullptr, 0, nullptr, 0, "Adjusting probabilities:", 4 }, + { "dump-priorities", OPT_DUMP_PRIORITIES, nullptr, 0, + "show current priorities, do not generate any formula", 0 }, + { "ltl-priorities", OPT_LTL_PRIORITIES, "STRING", 0, + "set priorities for LTL formulas", 0 }, + { "boolean-priorities", OPT_BOOLEAN_PRIORITIES, "STRING", 0, + "set priorities for Boolean formulas", 0 }, + { nullptr, 0, nullptr, 0, "STRING should be a comma-separated list of " + "assignments, assigning integer priorities to the tokens " + "listed by --dump-priorities.", 0 }, + /**************************************************/ + { nullptr, 0, nullptr, 0, "Output options:", -20 }, + { nullptr, 0, nullptr, 0, "The FORMAT string passed to --format may use " + "the following interpreted sequences:", -19 }, + { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the formula (in the selected syntax)", 0 }, + { "%l", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the (serial) number of the formula (0-based)", 0 }, + { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "the (serial) number of the formula (1-based)", 0 }, + { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "a single %", 0 }, + COMMON_LTL_OUTPUT_SPECS, + /**************************************************/ + { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, + { nullptr, 0, nullptr, 0, nullptr, 0 } +}; + +static const argp_child children[] = { + { &finput_argp, 0, nullptr, 0 }, + { &output_argp, 0, nullptr, 0 }, + { &misc_argp, 0, nullptr, 0 }, + { nullptr, 0, nullptr, 0 } +}; + +static int opt_formulas = 1; +static spot::randltlgenerator::output_type output = + spot::randltlgenerator::Bool; +static char* opt_pL = nullptr; +static char* opt_pB = nullptr; +static bool opt_dump_priorities = false; +static int opt_seed = 0; +static range opt_tree_size = { 5, 5 }; +static bool opt_unique = true; +static int opt_ap_count = 0; +static bool opt_literal = false; + +namespace +{ + // We want all these variables to be destroyed when we exit main, to + // make sure it happens before all other global variables (like the + // atomic propositions maps) are destroyed. Otherwise we risk + // accessing deleted stuff. + static struct opt_t + { + spot::atomic_prop_set sub; + }* opt = nullptr; + + class sub_processor final: public job_processor + { + public: + int + process_formula(spot::formula f, const char* filename = nullptr, + int linenum = 0) override + { + (void) filename; + (void) linenum; + opt->sub.insert(f); + return 0; + } + }; +} + +static sub_processor subreader; + +static int +parse_opt(int key, char* arg, struct argp_state*) +{ + // Called from C code, so should not raise any exception. + BEGIN_EXCEPTION_PROTECT; + switch (key) + { + case 'A': + opt_ap_count = to_int(arg, "-A/--ap-count"); + opt_literal = false; + break; + case 'B': + output = spot::randltlgenerator::Bool; + break; + case 'L': + output = spot::randltlgenerator::LTL; + break; + case 'n': + opt_formulas = to_int(arg, "-n/--formulas"); + break; + case 'P': + opt_ap_count = to_int(arg, "-P/--polarized-ap"); + opt_literal = true; + break; + case OPT_BOOLEAN_PRIORITIES: + opt_pB = arg; + break; + case OPT_LTL_PRIORITIES: + opt_pL = arg; + break; + case OPT_DUMP_PRIORITIES: + opt_dump_priorities = true; + break; + case OPT_DUPS: + opt_unique = false; + break; + case OPT_SEED: + opt_seed = to_int(arg, "--seed"); + break; + case OPT_TREE_SIZE: + opt_tree_size = parse_range(arg); + if (opt_tree_size.min > opt_tree_size.max) + std::swap(opt_tree_size.min, opt_tree_size.max); + break; + case ARGP_KEY_ARG: + jobs.emplace_back(arg, job_type::LTL_FILENAME); + break; + default: + return ARGP_ERR_UNKNOWN; + } + END_EXCEPTION_PROTECT; + return 0; +} + +int +main(int argc, char* argv[]) +{ + return protected_main(argv, [&] { + const argp ap = { options, parse_opt, "[FILENAME[/COL]...]", + argp_program_doc, children, nullptr, nullptr }; + + // This will ensure that all objects stored in this struct are + // destroyed before global variables. + opt_t o; + opt = &o; + + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) + exit(err); + + check_no_formula("combine"); + + if (subreader.run()) + return 2; + + if (opt->sub.empty()) + error(2, 0, "the set of subformulas to build from is empty"); + + spot::srand(opt_seed); + + spot::randltlgenerator rg + (opt_ap_count, + [&] (){ + spot::option_map opts; + opts.set("output", output); + opts.set("tree_size_min", opt_tree_size.min); + opts.set("tree_size_max", opt_tree_size.max); + opts.set("seed", opt_seed); + opts.set("simplification_level", 0); + opts.set("unique", opt_unique); + opts.set("literals", opt_literal); + return opts; + }(), opt_pL, nullptr, opt_pB, &opt->sub); + + if (opt_dump_priorities) + { + switch (output) + { + case spot::randltlgenerator::LTL: + std::cout << + "Use --ltl-priorities to set the following LTL priorities:\n"; + rg.dump_ltl_priorities(std::cout); + break; + case spot::randltlgenerator::Bool: + std::cout << + "Use --boolean-priorities to set the following Boolean " + "formula priorities:\n"; + rg.dump_bool_priorities(std::cout); + break; + case spot::randltlgenerator::PSL: + case spot::randltlgenerator::SERE: + error(2, 0, "PSL/SERE output is unsupported"); + break; + } + exit(0); + } + + int count = 0; + while (opt_formulas < 0 || opt_formulas--) + { + spot::formula f = rg.next(); + if (!f) + { + error(2, 0, "failed to generate a new unique formula after %d " \ + "trials", spot::randltlgenerator::MAX_TRIALS); + } + else + { + output_formula_checked(f, nullptr, nullptr, count + 1, count); + ++count; + } + }; + + flush_cout(); + return 0; + }); +} diff --git a/bin/man/Makefile.am b/bin/man/Makefile.am index 1b6319766..2ccf4b8b1 100644 --- a/bin/man/Makefile.am +++ b/bin/man/Makefile.am @@ -35,6 +35,7 @@ dist_man1_MANS = \ ltldo.1 \ ltlfilt.1 \ ltlgrind.1 \ + ltlmix.1 \ ltlsynt.1 \ randaut.1 \ randltl.1 @@ -72,6 +73,9 @@ ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc ltlgrind.1: $(common_dep) $(srcdir)/ltlgrind.x $(srcdir)/../ltlgrind.cc $(convman) ../ltlgrind$(EXEEXT) $(srcdir)/ltlgrind.x $@ +ltlmix.1: $(common_dep) $(srcdir)/ltlmix.x $(srcdir)/../ltlmix.cc + $(convman) ../ltlmix$(EXEEXT) $(srcdir)/ltlmix.x $@ + ltlsynt.1: $(common_dep) $(srcdir)/ltlsynt.x $(srcdir)/../ltlsynt.cc $(convman) ../ltlsynt$(EXEEXT) $(srcdir)/ltlsynt.x $@ diff --git a/bin/man/genltl.x b/bin/man/genltl.x index 6194ba8ab..db40c653b 100644 --- a/bin/man/genltl.x +++ b/bin/man/genltl.x @@ -80,3 +80,4 @@ Proceedings of RV'10. LNCS 6418. .BR ltlfilt (1), .BR randaut (1), .BR randltl (1) +.BR ltlmix (1) diff --git a/bin/man/ltlmix.x b/bin/man/ltlmix.x new file mode 100644 index 000000000..dbdc2f9f5 --- /dev/null +++ b/bin/man/ltlmix.x @@ -0,0 +1,7 @@ +[NAME] +ltlmix \- combine formulas selected randomly +[DESCRIPTION] +.\" Add any additional description here +[SEE ALSO] +.BR randltl (1), +.BR genltl (1) diff --git a/bin/man/randltl.x b/bin/man/randltl.x index cce4714fb..c9ab79c80 100644 --- a/bin/man/randltl.x +++ b/bin/man/randltl.x @@ -14,3 +14,4 @@ Proceedings of ATVA'13. LNCS 8172. .BR genltl (1), .BR ltlfilt (1), .BR randaut (1) +.BR ltlmix (1) diff --git a/bin/man/spot.x b/bin/man/spot.x index 037069d39..428839987 100644 --- a/bin/man/spot.x +++ b/bin/man/spot.x @@ -22,6 +22,7 @@ that are listed below. .BR ltldo (1) .BR ltlfilt (1) .BR ltlgrind (1) +.BR ltlmix (1) .BR ltlsynt (1) .BR randaut (1) .BR randltl (1) diff --git a/bin/spot.cc b/bin/spot.cc index 75401ddbc..e8be7f42a 100644 --- a/bin/spot.cc +++ b/bin/spot.cc @@ -37,6 +37,8 @@ static const argp_option options[] = { DOC("ltlgrind", "Mutate LTL or PSL formulas to generate similar but " "simpler ones. Use this when looking for shorter formula to " "reproduce a bug.") }, + { DOC("ltlmix", + "Combine LTL/PSL formulas taken randomly from some input set.") }, { nullptr, 0, nullptr, 0, "Tools that output automata or circuits:", 0 }, { DOC("randaut", "Generate random ω-automata.") }, { DOC("genaut", "Generate ω-automata from scalable patterns.") }, diff --git a/doc/Makefile.am b/doc/Makefile.am index 7abe05f9e..5b8e7edac 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -104,6 +104,7 @@ ORG_FILES = \ org/ltldo.org \ org/ltlfilt.org \ org/ltlgrind.org \ + org/ltlmix.org \ org/ltlsynt.org \ org/ltlsynt.tex \ org/oaut.org \ diff --git a/doc/org/arch.tex b/doc/org/arch.tex index 0e9e97e4a..f94df93e1 100644 --- a/doc/org/arch.tex +++ b/doc/org/arch.tex @@ -22,18 +22,19 @@ usedby/.style={->,ultra thick,>={Stealth[length=5mm,round]},gray!50!black}} \node[cppbox=14.12cm] (libspot) {\texttt{libspot\strut}}; \node[shbox=3cm,above right=2mm and 0mm of libspot.north west,align=center] (shcmd) { - \href{https://spot.lrde.epita.fr/randltl.html}{\texttt{randltl}}\\ - \href{https://spot.lrde.epita.fr/ltlfilt.html}{\texttt{ltlfilt}}\\ - \href{https://spot.lrde.epita.fr/randaut.html}{\texttt{randaut}}\\ - \href{https://spot.lrde.epita.fr/autfilt.html}{\texttt{autfilt}}\\ - \href{https://spot.lrde.epita.fr/ltl2tgba.html}{\texttt{ltl2tgba}}\\ - \href{https://spot.lrde.epita.fr/ltl2tgta.html}{\texttt{ltl2tgta}}\\ - \href{https://spot.lrde.epita.fr/dstar2tgba.html}{\texttt{dstar2tgba}}\\ - \href{https://spot.lrde.epita.fr/ltlcross.html}{\texttt{ltlcross}}\\ - \href{https://spot.lrde.epita.fr/ltlgrind.html}{\texttt{ltlgrind}}\\ - \href{https://spot.lrde.epita.fr/ltlsynt.html}{\texttt{ltlsynt}}\\ - \href{https://spot.lrde.epita.fr/ltldo.html}{\texttt{ltldo}}\\ - \href{https://spot.lrde.epita.fr/autcross.html}{\texttt{autcross}} + \href{https://spot.lre.epita.fr/randltl.html}{\texttt{randltl}}\\ + \href{https://spot.lre.epita.fr/ltlmix.html}{\texttt{ltlmix}}\\ + \href{https://spot.lre.epita.fr/ltlfilt.html}{\texttt{ltlfilt}}\\ + \href{https://spot.lre.epita.fr/randaut.html}{\texttt{randaut}}\\ + \href{https://spot.lre.epita.fr/autfilt.html}{\texttt{autfilt}}\\ + \href{https://spot.lre.epita.fr/ltl2tgba.html}{\texttt{ltl2tgba}}\\ + \href{https://spot.lre.epita.fr/ltl2tgta.html}{\texttt{ltl2tgta}}\\ + \href{https://spot.lre.epita.fr/dstar2tgba.html}{\texttt{dstar2tgba}}\\ + \href{https://spot.lre.epita.fr/ltlcross.html}{\texttt{ltlcross}}\\ + \href{https://spot.lre.epita.fr/ltlgrind.html}{\texttt{ltlgrind}}\\ + \href{https://spot.lre.epita.fr/ltlsynt.html}{\texttt{ltlsynt}}\\ + \href{https://spot.lre.epita.fr/ltldo.html}{\texttt{ltldo}}\\ + \href{https://spot.lre.epita.fr/autcross.html}{\texttt{autcross}} }; \node[cppbox=4.7cm,above right=0mm and 2mm of shcmd.south east] (libgen) {\texttt{libspotgen\strut}}; \node[cppbox=2.5cm,above right=0mm and 2mm of libgen.south east] (buddy) {\texttt{libbddx\strut}}; @@ -41,8 +42,8 @@ \node[cppbox=4cm,above right=0mm and 2mm of pyspot.south east] (libltsmin) {\texttt{libspotltsmin\strut}}; \node[shbox=1.5cm,above right=2mm and 0mm of libgen.north west,align=center] (genaut) { - \href{https://www.lrde.epita.fr/genaut.html}{\texttt{genaut\strut}}\\ - \href{https://www.lrde.epita.fr/genltl.html}{\texttt{genltl}} + \href{https://www.lre.epita.fr/genaut.html}{\texttt{genaut\strut}}\\ + \href{https://www.lre.epita.fr/genltl.html}{\texttt{genltl}} }; \node[pybox=3cm,above left=2mm and 0mm of libgen.north east] (pygen) {\texttt{import spot.gen\strut}}; diff --git a/doc/org/concepts.org b/doc/org/concepts.org index c4de7a324..d7ce0a57e 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -158,7 +158,7 @@ $txt #+END_SRC #+RESULTS: -[[file:concept-buchi.svg]] +[[file:concept-buchi2.svg]] The =1= displayed on the edge that loops on state =1= should be read as /true/, i.e., the Boolean formula that accepts diff --git a/doc/org/ltlmix.org b/doc/org/ltlmix.org new file mode 100644 index 000000000..338122d41 --- /dev/null +++ b/doc/org/ltlmix.org @@ -0,0 +1,365 @@ +# -*- coding: utf-8 -*- +#+TITLE: =ltlgrind= +#+DESCRIPTION: Spot command-line tool for combining LTL formulas randomly +#+INCLUDE: setup.org +#+HTML_LINK_UP: tools.html +#+PROPERTY: header-args:sh :results verbatim :exports both + +This tool creates new formulas by combining formulas randomly selected +from an input set of formulas. Some authors have argued that for some +tasks, like [[https://www.cs.rice.edu/~vardi/papers/time13.pdf][LTL satisfiability]], working with randomly generated +formulas is often easy, because random formulas tend to simplify +trivially. =ltlmix= allows you to take a set of formulas, usually +some handwritten, meaningful formulas, and combine those formulas to +build larger sets that are possibly more challenging. + +Here is a very simple example that builds five formulas that are +Boolean combination of formulas from taken in the set +$\{\mathsf{GF}a,\mathsf{FG}b,\mathsf{X}c\}$: + +#+BEGIN_SRC sh :exports both +ltlmix -f GFa -f FGb -f Xc -n 5 +#+END_SRC + +#+RESULTS: +: !FGb xor !Xc +: !GFa -> !FGb +: FGb | (FGb -> Xc) +: FGb +: GFa & (FGb | Xc) + +* Shape of the generated formulas + +** Size of the syntax tree + +For each formula that it generates, =ltlmix= constructs a random +syntax-tree of a certain size (5 by default) in which internal nodes +represent operators selected randomly from a list of operator, and +leaves are subformulas selected randomly from the set of input +formulas. As an example, the syntax tree of =!φ₁ xor !φ₂= has size 5, +and its leaves =φ₁= and =φ₂= will be taken randomly from the set of +input formulas. + +The algorithm is actually the same as for =randltl=, except +that =randltl= use random atomic propositions as leaves when =ltlmix= +uses random formulas. + +The same input formula can be picked several times to be used on +multiple leaves of the tree. Note that because Spot implements some +trivial rewritings directly during the construction of any formula, +formulas like =FGb | !!FGb= (which correspond to a tree of size 5 in +the above example) cannot be represented: they are automatically +simplified to =FGb=. Similarly, something like =φ xor φ= will be +output as =0=. + +The size of the tree can be changed using the =--tree-size= option. + +#+BEGIN_SRC sh :exports both + for i in 1 2 3 4 5 6 7 8 9 10 11 12; do + ltlmix -fXa -fGb -fFc -fXd -fGe --tree-size=$i + done +#+END_SRC + +#+RESULTS: +#+begin_example +Fc +!Xd +0 +Ge xor !Fc +!Xd xor !Ge +!Xd xor (Fc | Xd) +!Ge +Ge xor (!Ge -> Gb) +Ge xor (!Xa -> !Fc) +(Ge & !Fc) xor (!Gb xor !Ge) +(Ge & !Fc) xor (!Gb xor (Gb | Fc)) +(Ge & (Gb xor Xd)) xor (!Fc -> (Gb | Fc)) +#+end_example + +The above shows that while the size of the syntax tree generally grows +along with =--tree-size= there are several cases where it reduces +trivially. + +** Operator priorities + +It is possible to control the set of operators used in the generation. +The first step is to obtain that list of operators with =--dump-priorities=. +For instance: + +#+BEGIN_SRC sh :exports both + ltlmix -fXa -fGb -fFc -fXd -fGe --dump-priorities +#+END_SRC + +#+RESULTS: +#+begin_example +Use --boolean-priorities to set the following Boolean formula priorities: +sub 5 +false 0 +true 0 +not 1 +equiv 1 +implies 1 +xor 1 +and 1 +or 1 +#+end_example + +In the above list, =false= and =true= represent the Boolean constants +(which are usually undesirable when building random Boolean formulas), +and =sub= represent a random formula drawn from the list of input +formulas. + +The above command shows that each operator has a weight, called +/priority/. When the priority is 0, the operator is never used. When +=ltlmix= generates a syntax tree of size N, it looks among all +operators that can be used at the root of such a tree, and performs a +weighted random selection. In other words, an operator with priority +=2= will be twice more likely to be selected than an operator with +priority =1=. + +Those priorities can be changed with =--boolean-priorities= as in the +following example, which disables =xor= and makes =<->= thrice more +likely to appear. + +#+BEGIN_SRC sh :exports both + for i in 1 2 3 4 5 6 7 8 9 10 11 12; do + ltlmix -fXa -fGb -fFc -fXd -fGe --tree-size=$i --boolean-prio='xor=0,equiv=3' + done +#+END_SRC + +#+RESULTS: +#+begin_example +Fc +!Xd +1 +Ge <-> !Fc +!Xd <-> !Ge +!Xd <-> (Fc | Xd) +Ge +Ge <-> (Gb <-> !Ge) +Ge <-> (!Fc <-> !Xa) +(Ge & !Fc) <-> (!Ge -> !Gb) +(Ge & !Fc) <-> ((Gb | Fc) -> !Gb) +(Ge & (Gb <-> Xd)) <-> ((Gb | Fc) <-> !Fc) +#+end_example + +** Boolean or LTL syntax tree + +By default, the syntax tree generated on top of the randomly selected +input formula uses only Boolean operators. + +Using option =-L= will use LTL operators instead. + +#+BEGIN_SRC sh :exports both + ltlmix -fXa -fGb -fFc --tree-size=10 -L -n10 +#+END_SRC + +#+RESULTS: +#+begin_example +Gb R (XFc W 0) +!(Gb | !Xa) +1 U !X(0) +(Xa xor Gb) -> (GXa M Fc) +GFc M 1 +(Fc U Gb) -> (0 R Xa) +!Gb <-> (Gb | GFc) +1 +GFc | (1 U Xa) +!(Xa | GFc) +#+end_example + +The following operators are used: + +#+BEGIN_SRC sh :exports both + ltlmix -fXa -fGb -fFc -fXd -fGe -L --dump-priorities +#+END_SRC + +#+RESULTS: +#+begin_example +Use --ltl-priorities to set the following LTL priorities: +sub 5 +false 1 +true 1 +not 1 +F 1 +G 1 +X 1 +equiv 1 +implies 1 +xor 1 +R 1 +U 1 +W 1 +M 1 +and 1 +or 1 +#+end_example + +Note that in the LTL case, =false= and =true= can be generated by default. + +* Randomizing atomic propositions with =-A= or =-P= + +Options =-A= or =-P= can be used to change the atomic propositions +used in the input formulas. This works as follows: if =-A N= was +given, every time an input formula φ is selected, its atomic +propositions are replaced by atomic propositions randomly selected in +a set of size $N$. If φ uses $i$ atomic propositions and $i\ge N$, +then those $i$ atomic proposition will be remapped to $i$ distinct +atomic propositions chosen randomly in that set. if $i>N$, some of +the new atomic propositions may replace several of the original atomic +propositions. + +Option =-P N= is similar to =-A N= except that the selected atomic +propositions can possibly be negated. + + +These options solve two problems: + +- They lessen the issue that a formula selected several times can lead + to syntax tree such as =φ | φ | φ= that reduces to =φ=. Now, each + occurrence of =φ= as a chance to use different atomic propositions. + (the larger =N= is, the more likely it is that these copies of φ + will be different). + +- They allow combining formulas that had completely different sets of + atomic propositions, in such a way that they are now interdependent + (the smaller N is the more likely it is that subformulas will share + atomic propositions). + + +Here is an example with a single formula, =GFa=, whose atomic proposition +will be randomly replaced by one of $\{p_0,p_1,p_2,p_3,p_4\}$. + +#+BEGIN_SRC sh :exports both + ltlmix -fGFa -A5 --tree-size=8 -n10 +#+END_SRC + +#+RESULTS: +#+begin_example +(GFp2 & GFp3) xor (!GFp0 xor GFp1) +(GFp4 -> GFp1) -> !GFp2 +!GFp4 | ((GFp2 & GFp3) -> GFp2) +!GFp2 | (GFp3 <-> (GFp2 & GFp1)) +!GFp0 | GFp4 +!(GFp2 & GFp1) <-> (GFp3 xor GFp0) +(GFp2 xor GFp0) | (GFp4 -> !GFp0) +(GFp4 | !GFp3) -> GFp4 +!GFp0 -> (GFp2 | GFp1) +!GFp1 <-> (!GFp2 xor !GFp1) +#+end_example + +Here is a similar example, with polarized atomic propositions instead: + +#+BEGIN_SRC sh :exports both + ltlmix -fGFa -P5 --tree-size=8 -n10 +#+END_SRC + +#+RESULTS: +#+begin_example +(GFp2 & GF!p3) xor (GFp4 -> !GF!p1) +(GFp4 | !GFp2) -> (GFp1 -> GF!p1) +!GF!p2 & (GF!p0 xor (GF!p0 -> GF!p3)) +GFp1 <-> (GF!p3 | !GFp0) +GF!p1 & GFp0 & (GF!p3 xor !GF!p4) +(GF!p1 xor GF!p2) | (GF!p3 & !GF!p4) +!(GFp4 xor (!GF!p2 | !GF!p3)) +GFp0 | (!GFp1 -> (GFp1 -> GF!p4)) +GF!p1 xor (!GF!p2 | (GF!p1 <-> GFp0)) +!((GF!p2 <-> GF!p4) & (GFp1 xor GF!p2)) +#+end_example + + +* More serious examples + +** Mixing the DAC patterns + +The command [[file:genltl.org][=genltl --dac-pattern=]] will print a list of 55 LTL +formulas representing various specification patterns listed by Dwyer +et al. (FMSP'98). Using =--stat=%x= to count the atomic propositions +in each formula, and some standard unix tools, we can compute that +they use at most 6 atomic propositions. + +#+BEGIN_SRC sh :exports both + genltl --dac-pattern --stat=%x | sort -n | tail -n 1 +#+END_SRC +#+RESULTS: +: 6 + +Based on this, we could decide to generate Boolean combination of +those formulas while replacing atomic propositions by literals built +out of a set of 10 atomic propositions (chosen larger than 6 to ensure +that each individual formula will still make sense after the change of +atomic propositions). + +#+BEGIN_SRC sh :exports both + genltl --dac-pattern | ltlmix -n8 -P10 +#+END_SRC + +#+RESULTS: +: !G((p8 & F!p7) -> (!p4 U (!p7 | (!p2 & !p4 & X(!p4 U p1))))) xor !G(!p3 -> ((p4 & !p7) U (!p4 | ((p4 & p7) U (!p4 | ((p4 & !p7) U (!p4 | ((p4 & p7) U (!p4 | (!p7 W !p4) | Gp7))))))))) +: !G(!p3 -> Gp5) xor !G(!p7 -> G(p9 -> (!p5 & !p8 & X(!p5 U p2)))) +: G(p6 -> ((!(!p1 & p7 & X(!p1 U (!p1 & !p3))) U (p1 | !p2)) | G!(p7 & XF!p3))) & (G((!p4 & XF!p5) -> XF(!p5 & F!p0)) <-> G((p5 & !p6) -> (p5 W (p5 & p7)))) +: !G((p0 & p9) -> (!p7 W (!p0 | p4))) & !G((p1 & !p2) -> (!p8 W p2)) +: ((Fp2 -> ((!p1 -> (!p2 U (p0 & !p2))) U p2)) -> G(p1 -> G(p9 -> (!p4 & p8 & X(!p4 U !p7))))) xor G(p1 -> Gp9) +: !G((p5 & !p9 & F!p5) -> ((!p8 -> (p5 U (!p0 & p5))) U !p5)) -> !G((p6 & p9) -> (!p7 W !p9)) +: G((!p1 & !p2) -> (p9 W p1)) <-> (G(p5 -> G(p0 -> F!p4)) -> (Fp6 -> ((!p5 & !p6) U (p6 | ((p5 & !p6) U (p6 | ((!p5 & !p6) U (p6 | ((p5 & !p6) U (p6 | (!p5 U p6))))))))))) +: ((Fp1 -> ((p6 -> (!p1 U (!p1 & !p2 & X(!p1 U !p9)))) U p1)) <-> (F!p0 -> (p0 U (p0 & !p7 & X(p0 U !p9))))) | (Fp2 -> (p6 U (p2 | (p6 & !p7 & X(p6 U p1))))) + +Now we might want to clean this list a bit by relabeling each formula +so is uses atomic propositions $\{p_0,p_1,...\}$ starting at 0 and without gap. + +#+BEGIN_SRC sh :exports both + genltl --dac-pattern | ltlmix -n8 -P10 | ltlfilt --relabel=pnn +#+END_SRC + +#+RESULTS: +: !G((p0 & F!p1) -> (!p2 U (!p1 | (!p2 & !p3 & X(!p2 U p4))))) xor !G(!p5 -> ((!p1 & p2) U (!p2 | ((p1 & p2) U (!p2 | ((!p1 & p2) U (!p2 | ((p1 & p2) U (!p2 | (!p1 W !p2) | Gp1))))))))) +: !G(!p0 -> Gp1) xor !G(!p2 -> G(p3 -> (!p1 & !p4 & X(!p1 U p5)))) +: G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & !p3))) U (p1 | !p4)) | G!(p2 & XF!p3))) & (G((!p5 & XF!p6) -> XF(!p6 & F!p7)) <-> G((!p0 & p6) -> (p6 W (p2 & p6)))) +: !G((p0 & p1) -> (!p2 W (!p0 | p3))) & !G((p4 & !p5) -> (!p6 W p5)) +: ((Fp0 -> ((!p1 -> (!p0 U (!p0 & p2))) U p0)) -> G(p1 -> G(p3 -> (!p4 & p5 & X(!p4 U !p6))))) xor G(p1 -> Gp3) +: !G((p0 & !p1 & F!p0) -> ((!p2 -> (p0 U (p0 & !p3))) U !p0)) -> !G((p1 & p4) -> (!p5 W !p1)) +: G((!p0 & !p1) -> (p2 W p0)) <-> (G(p3 -> G(p4 -> F!p5)) -> (Fp6 -> ((!p3 & !p6) U (p6 | ((p3 & !p6) U (p6 | ((!p3 & !p6) U (p6 | ((p3 & !p6) U (p6 | (!p3 U p6))))))))))) +: ((Fp0 -> ((p1 -> (!p0 U (!p0 & !p2 & X(!p0 U !p3)))) U p0)) <-> (F!p4 -> (p4 U (p4 & !p5 & X(p4 U !p3))))) | (Fp2 -> (p1 U (p2 | (p1 & !p5 & X(p1 U p0))))) + +** Random conjunctions + +Some benchmark (e.g., [[https://www.cs.rice.edu/~vardi/papers/time13.pdf][for LTL satisfiability]]) are built by conjunction +of $L$ random formulas picked from a set of basic formulas. Each +picked formula has its atomic proposition mapped to random literals +built from a subset of $m$ atomic variables. + +Given a value for $m$, option =-P m= will achieve the second part of +the above description. To build a conjunction of $L$ formulas, we +need to ask for a tree of size $2L-1$ in which only the =and= operator +is allowed. + +Here is an example with $L=10$ (hence =--tree-size=19=) and $m=50$. +The example use a small set of three basic formulas +$\{\mathsf{G}a,\mathsf{F}a,\mathsf{X}a\}$ for illustration, but in +practice you should replace these =-f= options by =-F FILENAME= +pointing to a file containing all the input formulas to select from. + +#+BEGIN_SRC sh :exports both + ltlmix -fGa -fFa -fXa -n10 -P50 \ + --tree-size=19 --boolean-prio=not=0,or=0,xor=0,equiv=0,implies=0 +#+END_SRC + +#+RESULTS: +#+begin_example +Xp27 & F!p21 & G!p19 & X!p26 & Fp4 & Gp43 & Fp39 & Fp7 +G!p28 & G!p30 & X!p34 & Fp21 & Gp3 & Fp6 & F!p18 & Xp5 & Fp8 & F!p12 +X!p32 & Xp9 & Gp4 & Xp48 & F!p48 & X!p6 & Fp5 & Xp20 & Fp28 & Fp26 +G!p46 & X!p14 & Fp29 & X!p36 & Fp12 & Xp47 & Fp42 & Gp14 & Fp19 +G!p28 & Fp21 & Fp36 & F!p0 & G!p14 & Xp21 & F!p28 & G!p21 & Gp21 & Gp40 +Gp3 & F!p48 & F!p28 & Xp7 & Gp8 & Xp42 & Gp0 & Xp36 & F!p2 & G!p0 +Xp36 & Xp46 & F!p31 & Xp11 & Xp26 & G!p9 & F!p36 & X!p12 & Fp15 & Xp18 +Xp9 & X!p33 & Fp44 & X!p13 & Gp37 & Xp19 & G!p43 & F!p34 & Gp36 & Gp10 +Xp27 & Xp5 & Fp28 & Xp18 & G!p13 & Gp35 & Gp38 & G!p45 & G!p48 & Gp12 +Xp7 & G!p48 & Xp14 & Fp24 & Xp43 & Fp47 & Fp14 & Gp30 & Xp23 & G!p31 +#+end_example + +Selecting 10 random conjuncts out of 3×50×2=300 possibilities has a +13.7% chance that at least 2 conjuncts will be identical (see [[https://en.wikipedia.org/wiki/Birthday_problem][Birthday +paradox]]), so because of Spot's trivial rewritings, some hove the above +formulas may have fewer than 10 conjuncts. diff --git a/doc/org/tools.org b/doc/org/tools.org index 46ca38ccd..e24258a19 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -41,6 +41,7 @@ corresponding commands are hidden. * Command-line tools - [[file:randltl.org][=randltl=]] Generate random LTL/PSL formulas. +- [[file:ltlmix.org][=ltlmix=]] Combine LTL/PSL formulas taken randomly from some input set. - [[file:ltlfilt.org][=ltlfilt=]] Filter, convert, and transform LTL/PSL formulas. - [[file:genltl.org][=genltl=]] Generate LTL formulas from scalable patterns. - [[file:ltl2tgba.org][=ltl2tgba=]] Translate LTL/PSL formulas into various types of automata. @@ -77,6 +78,7 @@ convenience, you can browse their HTML versions: [[./man/ltldo.1.html][=ltldo=]](1), [[./man/ltlfilt.1.html][=ltlfilt=]](1), [[./man/ltlgrind.1.html][=ltlgrind=]](1), +[[./man/ltlmix.1.html][=ltlmix=]](1), [[./man/ltlsynt.1.html][=ltlsynt=]](1), [[./man/randaut.1.html][=randaut=]](1), [[./man/randltl.1.html][=randltl=]](1), diff --git a/spot/tl/randomltl.cc b/spot/tl/randomltl.cc index e415535b2..913b60522 100644 --- a/spot/tl/randomltl.cc +++ b/spot/tl/randomltl.cc @@ -28,6 +28,45 @@ namespace spot { namespace { + // Rename atomic propositions in f using atomic propositions drawn + // randomly from \a ap. Avoid repetition if \a ap is large + // enough. If \a lit is true, change the polarity of the atomic + // proposition randomly. + static formula + randomize_ap(formula f, const atomic_prop_set* ap, bool lit) + { + std::vector randap(ap->begin(), ap->end()); + unsigned current_range = randap.size(); + std::map mapping; + + auto relabel = [&](formula f, auto self) -> formula + { + if (f.is(op::ap)) + { + // Did we already rename this AP? + if (auto it = mapping.find(f); it != mapping.end()) + return it->second; + + // If we exhausted all possible AP, start again + if (current_range == 0) + current_range = randap.size(); + + // + unsigned pos = mrand(current_range--); + formula ap = randap[pos]; + std::swap(randap[current_range], randap[pos]); + + if (lit && drand() < 0.5) + ap = formula::Not(ap); + + return mapping[f] = ap; + } + return f.map(self, self); + }; + return relabel(f, relabel); + } + + static formula ap_builder(const random_formula* rl, int n) { @@ -38,6 +77,20 @@ namespace spot return *i; } + static formula + pattern_builder(const random_formula* rl, int n) + { + assert(n == 1); + (void) n; + atomic_prop_set::const_iterator i = rl->patterns()->begin(); + std::advance(i, mrand(rl->patterns()->size())); + formula f = *i; + const atomic_prop_set* ap = rl->ap(); + if (ap && ap->size() > 0) + f = randomize_ap(f, ap, rl->draw_literals()); + return f; + } + static formula true_builder(const random_formula*, int n) { @@ -353,13 +406,28 @@ namespace spot } // Boolean formulae - random_boolean::random_boolean(const atomic_prop_set* ap) + random_boolean::random_boolean(const atomic_prop_set* ap, + const atomic_prop_set* patterns) : random_formula(9, ap) { - proba_[0].setup("ap", 1, ap_builder); - proba_[0].proba = ap_->size(); + if (patterns) + { + proba_[0].setup("sub", 1, pattern_builder); + patterns_ = patterns; + proba_[0].proba = patterns_->size(); + } + else + { + proba_[0].setup("ap", 1, ap_builder); + proba_[0].proba = ap_->size(); + } proba_[1].setup("false", 1, false_builder); proba_[2].setup("true", 1, true_builder); + if (patterns) + { + proba_[1].proba = 0.0; + proba_[2].proba = 0.0; + } proba_2_or_more_ = proba_2_ = proba_ + 3; proba_[3].setup("not", 2, unop_builder); proba_[4].setup("equiv", 3, binop_builder); @@ -373,10 +441,19 @@ namespace spot // LTL formulae void - random_ltl::setup_proba_() + random_ltl::setup_proba_(const atomic_prop_set* patterns) { - proba_[0].setup("ap", 1, ap_builder); - proba_[0].proba = ap_->size(); + if (patterns) + { + proba_[0].setup("sub", 1, pattern_builder); + patterns_ = patterns; + proba_[0].proba = patterns_->size(); + } + else + { + proba_[0].setup("ap", 1, ap_builder); + proba_[0].proba = ap_->size(); + } proba_[1].setup("false", 1, false_builder); proba_[2].setup("true", 1, true_builder); proba_2_or_more_ = proba_2_ = proba_ + 3; @@ -395,17 +472,18 @@ namespace spot proba_[15].setup("or", 3, multop_builder); } - random_ltl::random_ltl(const atomic_prop_set* ap) + random_ltl::random_ltl(const atomic_prop_set* ap, + const atomic_prop_set* patterns) : random_formula(16, ap) { - setup_proba_(); + setup_proba_(patterns); update_sums(); } random_ltl::random_ltl(int size, const atomic_prop_set* ap) : random_formula(size, ap) { - setup_proba_(); + setup_proba_(nullptr); // No call to update_sums(), this functions is always // called by the random_psl constructor. } @@ -428,7 +506,8 @@ namespace spot const option_map& opts, char* opt_pL, char* opt_pS, - char* opt_pB) + char* opt_pB, + const atomic_prop_set* subs) : opt_simpl_level_(opts.get("simplification_level", 3)), simpl_(tl_simplifier_options{opt_simpl_level_}) { @@ -439,6 +518,7 @@ namespace spot opt_tree_size_max_ = opts.get("tree_size_max", 15); opt_unique_ = opts.get("unique", 1); opt_wf_ = opts.get("wf", 0); + bool lit = opts.get("literals", 0); const char* tok_pL = nullptr; const char* tok_pS = nullptr; @@ -447,23 +527,25 @@ namespace spot switch (output_) { case randltlgenerator::LTL: - rf_ = new random_ltl(&aprops_); + rf_ = new random_ltl(&aprops_, subs); + rf_->draw_literals(lit); if (opt_pS) - throw std::invalid_argument("Cannot set sere priorities with " + throw std::invalid_argument("Cannot set SERE priorities with " "LTL output"); if (opt_pB) - throw std::invalid_argument("Cannot set boolean priorities with " + throw std::invalid_argument("Cannot set Boolean priorities with " "LTL output"); tok_pL = rf_->parse_options(opt_pL); break; case randltlgenerator::Bool: - rf_ = new random_boolean(&aprops_); + rf_ = new random_boolean(&aprops_, subs); + rf_->draw_literals(lit); tok_pB = rf_->parse_options(opt_pB); if (opt_pL) - throw std::invalid_argument("Cannot set ltl priorities with " + throw std::invalid_argument("Cannot set LTL priorities with " "Boolean output"); if (opt_pS) - throw std::invalid_argument("Cannot set sere priorities " + throw std::invalid_argument("Cannot set SERE priorities " "with Boolean output"); break; case randltlgenerator::SERE: @@ -471,7 +553,7 @@ namespace spot tok_pS = rs_->parse_options(opt_pS); tok_pB = rs_->rb.parse_options(opt_pB); if (opt_pL) - throw std::invalid_argument("Cannot set ltl priorities " + throw std::invalid_argument("Cannot set LTL priorities " "with SERE output"); break; case randltlgenerator::PSL: @@ -500,9 +582,10 @@ namespace spot const option_map& opts, char* opt_pL, char* opt_pS, - char* opt_pB) + char* opt_pB, + const atomic_prop_set* subs) : randltlgenerator(create_atomic_prop_set(aprops_n), opts, - opt_pL, opt_pS, opt_pB) + opt_pL, opt_pS, opt_pB, subs) { } @@ -602,4 +685,5 @@ namespace spot { rs_->rb.dump_priorities(os); } + } diff --git a/spot/tl/randomltl.hh b/spot/tl/randomltl.hh index a7ea3561c..8c2e7e0cd 100644 --- a/spot/tl/randomltl.hh +++ b/spot/tl/randomltl.hh @@ -44,16 +44,33 @@ namespace spot delete[] proba_; } - /// Return the set of atomic proposition used to build formulae. - const atomic_prop_set* - ap() const + /// Return the set of atomic proposition used to build formulas. + const atomic_prop_set* ap() const { return ap_; } + /// Return the set of patterns (sub-formulas) used to build formulas. + const atomic_prop_set* patterns() const + { + return patterns_; + } + + /// Check whether relabeling APs should use literals. + bool draw_literals() const + { + return draw_literals_; + } + + /// Set whether relabeling APs should use literals. + void draw_literals(bool lit) + { + draw_literals_ = lit; + } + /// \brief Generate a formula of size \a n. /// - /// It is possible to obtain formulae that are smaller than \a + /// It is possible to obtain formulas that are smaller than \a /// n, because some simple simplifications are performed by the /// AST. (For instance the formula a | a is /// automatically reduced to a by spot::multop.) @@ -63,7 +80,7 @@ namespace spot /// and atomic propositions. std::ostream& dump_priorities(std::ostream& os) const; - /// \brief Update the priorities used to generate the formulae. + /// \brief Update the priorities used to generate the formulas. /// /// \a options should be comma-separated list of KEY=VALUE /// assignments, using keys from the above list. @@ -98,14 +115,16 @@ namespace spot op_proba* proba_2_or_more_; double total_2_and_more_; const atomic_prop_set* ap_; + const atomic_prop_set* patterns_ = nullptr; + bool draw_literals_; }; /// \ingroup tl_io - /// \brief Generate random LTL formulae. + /// \brief Generate random LTL formulas. /// - /// This class recursively constructs LTL formulae of a given - /// size. The formulae will use the use atomic propositions from + /// This class recursively constructs LTL formulas of a given + /// size. The formulas will use the use atomic propositions from /// the set of propositions passed to the constructor, in addition /// to the constant and all LTL operators supported by Spot. /// @@ -118,25 +137,26 @@ namespace spot public: /// Create a random LTL generator using atomic propositions from \a ap. /// - /// The default priorities are defined as follows: + /// The default priorities are defined as follows, depending on the + /// presence of \a subformulas. /// /** \verbatim - ap n - false 1 - true 1 - not 1 - F 1 - G 1 - X 1 - equiv 1 - implies 1 - xor 1 - R 1 - U 1 - W 1 - M 1 - and 1 - or 1 + ap n sub n + false 1 false 1 + true 1 true 1 + not 1 not 1 + F 1 F 1 + G 1 G 1 + X 1 X 1 + equiv 1 equiv 1 + implies 1 implies 1 + xor 1 xor 1 + R 1 R 1 + U 1 U 1 + W 1 W 1 + M 1 M 1 + and 1 and 1 + or 1 or 1 \endverbatim */ /// /// Where \c n is the number of atomic propositions in the @@ -147,18 +167,25 @@ namespace spot /// as each constant (i.e., true and false) to be picked. /// /// These priorities can be changed use the parse_options method. - random_ltl(const atomic_prop_set* ap); + /// + /// If a set of subformulas is passed to the constructor, the generator + /// will build a Boolean formulas using patterns as atoms. Atomic + /// propositions in patterns will be rewritten randomly by drawing + /// some from \a ap. The probability of false/true to be generated + /// default to 0 in this case. + random_ltl(const atomic_prop_set* ap, + const atomic_prop_set* subformulas = nullptr); protected: - void setup_proba_(); + void setup_proba_(const atomic_prop_set* patterns); random_ltl(int size, const atomic_prop_set* ap); }; /// \ingroup tl_io - /// \brief Generate random Boolean formulae. + /// \brief Generate random Boolean formulas. /// - /// This class recursively constructs Boolean formulae of a given size. - /// The formulae will use the use atomic propositions from the + /// This class recursively constructs Boolean formulas of a given size. + /// The formulas will use the use atomic propositions from the /// set of propositions passed to the constructor, in addition to the /// constant and all Boolean operators supported by Spot. /// @@ -169,18 +196,19 @@ namespace spot /// Create a random Boolean formula generator using atomic /// propositions from \a ap. /// - /// The default priorities are defined as follows: + /// The default priorities are defined as follows depending on + /// the presence of \a subformulas. /// /** \verbatim - ap n - false 1 - true 1 - not 1 - equiv 1 - implies 1 - xor 1 - and 1 - or 1 + ap n sub n + false 1 false 0 + true 1 true 0 + not 1 not 1 + equiv 1 equiv 1 + implies 1 implies 1 + xor 1 xor 1 + and 1 and 1 + or 1 or 1 \endverbatim */ /// /// Where \c n is the number of atomic propositions in the @@ -191,14 +219,20 @@ namespace spot /// as each constant (i.e., true and false) to be picked. /// /// These priorities can be changed use the parse_options method. - random_boolean(const atomic_prop_set* ap); + /// + /// If a set of \a subformulas is passed to the constructor, the + /// generator will build a Boolean formulas using patterns as + /// atoms. Atomic propositions in patterns will be rewritten + /// randomly by drawing some from \a ap. + random_boolean(const atomic_prop_set* ap, + const atomic_prop_set* subformulas = nullptr); }; /// \ingroup tl_io /// \brief Generate random SERE. /// /// This class recursively constructs SERE of a given size. - /// The formulae will use the use atomic propositions from the + /// The formulas will use the use atomic propositions from the /// set of propositions passed to the constructor, in addition to the /// constant and all SERE operators supported by Spot. /// @@ -230,7 +264,7 @@ namespace spot /// These priorities can be changed use the parse_options method. /// /// In addition, you can set the properties of the Boolean - /// formula generator used to build Boolean subformulae using + /// formula generator used to build Boolean subformulas using /// the parse_options method of the \c rb attribute. random_sere(const atomic_prop_set* ap); @@ -238,10 +272,10 @@ namespace spot }; /// \ingroup tl_io - /// \brief Generate random PSL formulae. + /// \brief Generate random PSL formulas. /// - /// This class recursively constructs PSL formulae of a given size. - /// The formulae will use the use atomic propositions from the + /// This class recursively constructs PSL formulas of a given size. + /// The formulas will use the use atomic propositions from the /// set of propositions passed to the constructor, in addition to the /// constant and all PSL operators supported by Spot. class SPOT_API random_psl: public random_ltl @@ -249,7 +283,7 @@ namespace spot public: /// Create a random PSL generator using atomic propositions from \a ap. /// - /// PSL formulae are built by combining LTL operators, plus + /// PSL formulas are built by combining LTL operators, plus /// three operators (EConcat, UConcat, Closure) taking a SERE /// as parameter. /// @@ -287,11 +321,11 @@ namespace spot /// These priorities can be changed use the parse_options method. /// /// In addition, you can set the properties of the SERE generator - /// used to build SERE subformulae using the parse_options method + /// used to build SERE subformulas using the parse_options method /// of the \c rs attribute. random_psl(const atomic_prop_set* ap); - /// The SERE generator used to generate SERE subformulae. + /// The SERE generator used to generate SERE subformulas. random_sere rs; }; @@ -307,12 +341,14 @@ namespace spot randltlgenerator(int aprops_n, const option_map& opts, char* opt_pL = nullptr, char* opt_pS = nullptr, - char* opt_pB = nullptr); + char* opt_pB = nullptr, + const atomic_prop_set* subformulas = nullptr); randltlgenerator(atomic_prop_set aprops, const option_map& opts, char* opt_pL = nullptr, char* opt_pS = nullptr, - char* opt_pB = nullptr); + char* opt_pB = nullptr, + const atomic_prop_set* subformulas = nullptr); ~randltlgenerator(); @@ -345,4 +381,6 @@ namespace spot random_psl* rp_ = nullptr; random_sere* rs_ = nullptr; }; + + } diff --git a/tests/Makefile.am b/tests/Makefile.am index bffb79ff1..54abc1a73 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -176,6 +176,7 @@ TESTS_tl = \ core/kind.test \ core/remove_x.test \ core/ltlrel.test \ + core/ltlmix.test \ core/ltlgrind.test \ core/ltlcrossgrind.test \ core/ltlfilt.test \ diff --git a/tests/core/ltlmix.test b/tests/core/ltlmix.test new file mode 100755 index 000000000..dd279e4fa --- /dev/null +++ b/tests/core/ltlmix.test @@ -0,0 +1,93 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) by the Spot authors, see the AUTHORS file for details. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs || exit 1 + +set -e + +# Make sure sort isn't affected by the user's LC_COLLATE +LC_ALL=C +export LC_ALL + +ltlmix -fGa -fFb --tree-size=4 -n 50 -o out.ltl 2>stderr && exit 1 +grep 'failed to generate a new unique formula' stderr +test 34 -eq `wc -l < out.ltl` + +ltlmix -fGa -fFb --tree-size=4 -n 500 -L -o out.ltl 2>stderr && exit 1 +grep 'failed to generate a new unique formula' stderr +test 448 -eq `wc -l < out.ltl` + +P=--boolean-priorities=not=0,xor=0,equiv=0,implies=0 +ltlmix -fGa -fFb --tree-size=4 -n 10 $P -o out.ltl 2>stderr && exit 1 +grep 'failed to generate a new unique formula' stderr +test 4 -eq `wc -l < out.ltl` + +ltlmix -fa -A9 --tree-size=1 -n9 | sort > list1 +ltlmix -fa -P9 --tree-size=1 -n18 | sort > list2 +grep -v '!' list2 > list3 +diff list1 list3 + +# The following message appears only if run from a tty. +if (: > /dev/tty) >/dev/null 2>&1 ; then + ltlmix -A9 -n10 err && exit 2 + grep 'No formula to combine' err +fi + + +genltl --gf-equiv-xn=1..3 | ltlmix --tree-size=1 -A2 -n6 | sort >out +cat >expected < XXXp0) +GF(p0 <-> XXp0) +GF(p0 <-> Xp0) +GF(p1 <-> XXXp1) +GF(p1 <-> XXp1) +GF(p1 <-> Xp1) +EOF +diff out expected + + +genltl --and-gf=4 > in.ltl +ltlmix in.ltl --tree-size=1 -A1 --stats=%x > out.txt +ltlmix in.ltl --tree-size=1 -A2 --stats=%x >> out.txt +ltlmix in.ltl --tree-size=1 -A3 --stats=%x >> out.txt +ltlmix in.ltl --tree-size=1 -A4 --stats=%x >> out.txt +ltlmix in.ltl --tree-size=1 -A5 --stats=%x >> out.txt +ltlmix in.ltl --tree-size=1 -A6 --stats=%x >> out.txt + +cat >expected < out.txt +ltlmix in.ltl --tree-size=1 -P2 --stats=%x >> out.txt +ltlmix in.ltl --tree-size=1 -P3 --stats=%x >> out.txt +ltlmix in.ltl --tree-size=1 -P4 --stats=%x >> out.txt +ltlmix in.ltl --tree-size=1 -P5 --stats=%x >> out.txt +ltlmix in.ltl --tree-size=1 -P6 --stats=%x >> out.txt +diff out.txt expected + +ltlmix -fa -A500 $P,or=0 -n10 | tee out +test 10 -eq `grep '&.*&' < out | wc -l`