diff --git a/.gitignore b/.gitignore index 155a9b5e7..73745a48f 100644 --- a/.gitignore +++ b/.gitignore @@ -82,3 +82,4 @@ GTAGS *.dsc *.gcov spot.spec +default.nix diff --git a/Makefile.am b/Makefile.am index e198a977c..a5d842b4c 100644 --- a/Makefile.am +++ b/Makefile.am @@ -65,7 +65,8 @@ EXTRA_DIST = HACKING ChangeLog.1 tools/gitlog-to-changelog \ tools/help2man tools/man2html.pl \ tools/test-driver-teamcity $(UTF8) $(DEBIAN) \ m4/gnulib-cache.m4 .dir-locals.el \ - spot.spec spot.spec.in README.ltsmin + spot.spec spot.spec.in README.ltsmin \ + default.nix default.nix.in dist-hook: gen-ChangeLog @@ -111,3 +112,6 @@ deb: dist spot.spec: configure.ac spot.spec.in sed 's/[@]VERSION[@]/$(VERSION)/;s/[@]GITPATCH[@]/@@@$(GITPATCH)/;s/@@@\.//' spot.spec.in > $@.tmp && mv $@.tmp $@ + +default.nix: configure.ac default.nix.in + sed 's/[@]VERSION[@]/$(VERSION)/' default.nix.in > $@.tmp && mv $@.tmp $@ diff --git a/bin/common_post.cc b/bin/common_post.cc index fdb1dc903..7bead8135 100644 --- a/bin/common_post.cc +++ b/bin/common_post.cc @@ -231,7 +231,14 @@ parse_opt_post(int key, char* arg, struct argp_state*) if (arg) type = XARGMATCH(key == 'P' ? "--parity" : "--colored-parity", arg, parity_args, parity_types); - else + else if (!(type & spot::postprocessor::Parity)) + // If no argument was given, we just require Parity. + // However, if a Parity condition was already set before, + // don't overwrite it. This way if someone mistakenly write + // `--parity='max even' --colored` without realizing that + // `--colored` is just the abbreviation for + // `--colored-parity=...` with the default argument, we + // won't reset the 'max even' setting. type = spot::postprocessor::Parity; if (key == 'p') colored = spot::postprocessor::Colored; diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 4b5858c01..1b741fa9a 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -91,17 +91,15 @@ static const argp_option options[] = /**************************************************/ { nullptr, 0, nullptr, 0, "Fine tuning:", 10 }, { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old|acd", 0, - "choose the algorithm for synthesis:" - " \"sd\": translate to tgba, split, then determinize;" - " \"ds\": translate to tgba, determinize, then split;" - " \"ps\": translate to dpa, then split;" - " \"lar\": translate to a deterministic automaton with arbitrary" - " acceptance condition, then use LAR to turn to parity," - " then split (default);" - " \"lar.old\": old version of LAR, for benchmarking;" - " \"acd\": translate to a deterministic automaton with arbitrary" - " acceptance condition, then use ACD to turn to parity," - " then split.\n", 0 }, + "choose the algorithm for synthesis:\n" + " sd: translate to TGBA, split, determinize\n" + " ds: translate to TGBA, determinize, split\n" + " ps: translate to DPA, split\n" + " lar: translate to a deterministic TELA, convert to DPA" + " with LAR, split (default)\n" + " lar.old: old version of LAR, for benchmarking;\n" + " acd: translate to a deterministic TELA, convert to DPA" + " with ACD, split", 0 }, { "bypass", OPT_BYPASS, "yes|no", 0, "whether to try to avoid to construct a parity game " "(enabled by default)", 0}, diff --git a/default.nix.in b/default.nix.in new file mode 100644 index 000000000..8101e4f74 --- /dev/null +++ b/default.nix.in @@ -0,0 +1,35 @@ +# -*- mode: nix; coding: utf-8 -*- +# Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# 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 . + +{ pkgs ? import {} }: +let + version = "@VERSION@"; +in +pkgs.stdenv.mkDerivation { + inherit version; + pname = "spot"; + + buildInputs = [ + pkgs.python3 + ]; + + src = ./.; + + enableParallelBuilding = true; +} diff --git a/flake.lock b/flake.lock new file mode 100644 index 000000000..dd215f1c6 --- /dev/null +++ b/flake.lock @@ -0,0 +1,61 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1741196730, + "narHash": "sha256-0Sj6ZKjCpQMfWnN0NURqRCQn2ob7YtXTAOTwCuz7fkA=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "48913d8f9127ea6530a2a2f1bd4daa1b8685d8a3", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-24.11", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 000000000..f0f3f95b5 --- /dev/null +++ b/flake.nix @@ -0,0 +1,214 @@ +{ + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11"; + flake-utils.url = "github:numtide/flake-utils"; + }; + outputs = { self, nixpkgs, flake-utils, ... }: + flake-utils.lib.eachSystem + [ + "x86_64-linux" + ] + + (system: + let + pkgs = import nixpkgs { inherit system; }; + lib = pkgs.lib; + + mkSpotApps = appNames: + pkgs.lib.genAttrs appNames + (name: flake-utils.lib.mkApp { + drv = self.packages.${system}.spot; + name = name; + }); + + spotPackage = + let + inherit (builtins) + filter + head + isString + match + readFile + split + ; + + # NOTE: Maintaining the version separately would be a pain, and we + # can't have a flake.nix.in with a @VERSION@ because it would make + # the flake unusable without running autoconf first, defeating some + # of its purpose. + # + # So let's get it the hard way instead :) + extractVersionRegex = ''^AC_INIT\(\[spot], \[([^]]+)], \[spot@lrde\.epita\.fr]\)$''; + getLines = (fileContent: + filter isString (split "\n" fileContent) + ); + findVersionLine = (lines: + lib.lists.findFirst + (l: lib.strings.hasPrefix "AC_INIT(" l) + null + lines + ); + getVersion = (file: + let + lines = getLines (readFile file); + versionLine = findVersionLine lines; + version = head (match extractVersionRegex versionLine); + in + version + ); + in + { + lib, + pkgs, + stdenv, + # FIXME: do we want this flag? + buildOrgDoc ? false, + # Whether to enable Spot's Python 3 bindings + enablePython ? false + }: + stdenv.mkDerivation { + pname = "spot"; + version = getVersion ./configure.ac; + + src = self; + + enableParallelBuilding = true; + + # NOTE: Nix enables a lot of hardening flags by default, some of + # these probably harm performance so I've disabled everything + # (haven't benchmarked with vs without these, though). + hardeningDisable = [ "all" ]; + + # NOTE: mktexpk fails without a HOME set + preBuild = '' + export HOME=$TMPDIR + patchShebangs tools + '' + (if buildOrgDoc then '' + ln -s ${pkgs.plantuml}/lib/plantuml.jar doc/org/plantuml.jar + '' else '' + touch doc/org-stamp + ''); + + configureFlags = [ + "--disable-devel" + "--enable-optimizations" + ] ++ lib.optional (!enablePython) [ + "--disable-python" + ]; + + nativeBuildInputs = with pkgs; [ + autoreconfHook + + autoconf + automake + bison + flex + libtool + perl + ] ++ lib.optional buildOrgDoc [ + graphviz + groff + plantuml + pdf2svg + R + ] ++ lib.optional enablePython [ + python3 + swig4 + ]; + + buildInputs = with pkgs; [ + # should provide the minimum amount of packages necessary for + # building tl.pdf + (texlive.combine { + inherit (texlive) + scheme-basic + latexmk + + booktabs + cm-super + doi + doublestroke + etoolbox + koma-script + mathabx-type1 + mathpazo + metafont + microtype + nag + pgf + standalone + stmaryrd + tabulary + todonotes + wasy-type1 + wasysym + ; + }) + ]; + }; + in + { + defaultPackage = self.packages.${system}.spot; + + packages = { + # binaries + library only + spot = pkgs.callPackage spotPackage {}; + + # NOTE: clang build is broken on Nix when linking to stdlib++, using + # libcxx instead. See: + # https://github.com/NixOS/nixpkgs/issues/91285 + spotClang = pkgs.callPackage spotPackage { + stdenv = pkgs.llvmPackages.libcxxStdenv; + }; + + spotWithOrgDoc = pkgs.callPackage spotPackage { + buildOrgDoc = true; + }; + + spotWithPython = pkgs.python3Packages.toPythonModule ( + pkgs.callPackage spotPackage { + enablePython = true; + } + ); + + spotFull = pkgs.python3Packages.toPythonModule ( + pkgs.callPackage spotPackage { + buildOrgDoc = true; enablePython = true; + } + ); + }; + + apps = mkSpotApps [ + "autcross" + "autfilt" + "dstar2tgba" + "genaut" + "genltl" + "ltl2tgba" + "ltl2tgta" + "ltlcross" + "ltldo" + "ltlfilt" + "ltlgrind" + "ltlmix" + "ltlsynt" + "randaut" + "randltl" + ]; + + devShell = pkgs.mkShell { + name = "spot-dev"; + inputsFrom = [ self.packages.${system}.spotFull ]; + buildInputs = [ + pkgs.gdb + pkgs.clang-tools # for clangd + pkgs.bear + + (pkgs.python3.withPackages (p: [ + p.jupyter + p.ipython # otherwise ipython module isn't found when running ipynb tests + ])) + ]; + }; + }); +} diff --git a/python/spot/impl.i b/python/spot/impl.i index 2291730ed..a435758f6 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -86,7 +86,10 @@ #include #include +#include #include +#include +#include #include #include #include @@ -162,6 +165,7 @@ #include #include #include +#include #include #include #include @@ -544,6 +548,8 @@ namespace std { %template(vectorofvectorofformulas) vector>; %template(setunsigned) set; %template(relabeling_map) map; + %template(pair_formula) pair; + %template(vector_pair_formula) vector>; } %include @@ -631,6 +637,9 @@ namespace std { %include %include +%include +%include +%include %include %include %include @@ -788,6 +797,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot.spec.in b/spot.spec.in index bd465fd62..a2630d2de 100755 --- a/spot.spec.in +++ b/spot.spec.in @@ -38,6 +38,7 @@ logic (LTL & PSL). %{_bindir}/ltldo %{_bindir}/ltlfilt %{_bindir}/ltlgrind +%{_bindir}/ltlmix %{_bindir}/ltlsynt %{_bindir}/randaut %{_bindir}/randltl @@ -52,11 +53,12 @@ logic (LTL & PSL). %{_mandir}/man1/ltldo.1* %{_mandir}/man1/ltlfilt.1* %{_mandir}/man1/ltlgrind.1* +%{_mandir}/man1/ltlmix.1* %{_mandir}/man1/ltlsynt.1* %{_mandir}/man1/randaut.1* %{_mandir}/man1/randltl.1* -%{_mandir}/man7/spot-x.7* %{_mandir}/man7/spot.7* +%{_mandir}/man7/spot-x.7* %license COPYING %doc AUTHORS COPYING NEWS README THANKS diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 3b43f751b..16d117ffc 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -557,10 +557,11 @@ namespace spot { std::map, unsigned> uniq_; G& g_; + unsigned acc_sink_; public: - univ_dest_mapper(G& graph) - : g_(graph) + univ_dest_mapper(G& graph, unsigned sink = -1u) + : g_(graph), acc_sink_(sink) { } @@ -570,6 +571,9 @@ namespace spot std::vector tmp(begin, end); std::sort(tmp.begin(), tmp.end()); tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end()); + if (acc_sink_ != -1u && tmp.size() > 1) + tmp.erase(std::remove(tmp.begin(), tmp.end(), acc_sink_), + tmp.end()); auto p = uniq_.emplace(tmp, 0); if (p.second) p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end()); diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am index 6c7650875..f2ff0fcad 100644 --- a/spot/tl/Makefile.am +++ b/spot/tl/Makefile.am @@ -28,9 +28,11 @@ tl_HEADERS = \ declenv.hh \ defaultenv.hh \ delta2.hh \ + derive.hh \ dot.hh \ environment.hh \ exclusive.hh \ + expansions2.hh \ formula.hh \ hierarchy.hh \ length.hh \ @@ -54,8 +56,11 @@ libtl_la_SOURCES = \ declenv.cc \ defaultenv.cc \ delta2.cc \ + derive.cc \ dot.cc \ exclusive.cc \ + expansions.cc \ + expansions2.cc \ formula.cc \ hierarchy.cc \ length.cc \ diff --git a/spot/tl/derive.cc b/spot/tl/derive.cc new file mode 100644 index 000000000..5e8526eec --- /dev/null +++ b/spot/tl/derive.cc @@ -0,0 +1,589 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// 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 "config.h" +#include +#include +#include +#include +#include + +namespace spot +{ + namespace + { + static std::pair + first(formula f, const bdd_dict_ptr& d, void* owner) + { + if (f.is_boolean()) + { + bdd res = formula_to_bdd(f, d, owner); + return { res, bdd_support(res) }; + } + + switch (f.kind()) + { + // handled by is_boolean above + case op::ff: + case op::tt: + case op::ap: + case op::And: + case op::Or: + SPOT_UNREACHABLE(); + + case op::eword: + return { bddfalse, bddtrue }; + + case op::OrRat: + { + bdd res = bddfalse; + bdd support = bddtrue; + for (auto subformula : f) + { + auto [r, sup] = first(subformula, d, owner); + res |= r; + support &= sup; + } + return { res, support }; + } + + case op::AndRat: + { + bdd res = bddtrue; + bdd support = bddtrue; + for (auto subformula : f) + { + auto [r, sup] = first(subformula, d, owner); + res &= r; + support &= sup; + } + return { res, support }; + } + + case op::AndNLM: + return first(rewrite_and_nlm(f), d, owner); + + case op::Concat: + { + auto [res, support] = first(f[0], d, owner); + + if (f[0].accepts_eword()) + { + auto [r, sup] = first(f.all_but(0), d, owner); + res |= r; + support &= sup; + } + + return { res, support }; + } + + case op::Fusion: + { + auto [res, support] = first(f[0], d, owner); + + // this should be computed only if f[0] recognizes words of size 1 + // or accepts eword ? + auto p = first(f.all_but(0), d, owner); + + return { res, support & p.second }; + } + + case op::Star: + case op::first_match: + return first(f[0], d, owner); + + case op::FStar: + { + auto [res, support] = first(f[0], d, owner); + + if (f.min() == 0) + res = bddtrue; + + return { res, support }; + } + + default: + std::cerr << "unimplemented kind " + << static_cast(f.kind()) + << std::endl; + SPOT_UNIMPLEMENTED(); + } + + return { bddfalse, bddtrue }; + } + + static std::vector + formula_aps(formula f) + { + auto res = std::unordered_set(); + + f.traverse([&res](formula f) + { + if (f.is(op::ap)) + { + res.insert(f.ap_name()); + return true; + } + + return false; + }); + + return std::vector(res.begin(), res.end()); + } + } + + formula + rewrite_and_nlm(formula f) + { + unsigned s = f.size(); + std::vector final; + std::vector non_final; + + for (auto g: f) + if (g.accepts_eword()) + final.emplace_back(g); + else + non_final.emplace_back(g); + + if (non_final.empty()) + // (a* & b*);c = (a*|b*);c + return formula::OrRat(std::move(final)); + if (!final.empty()) + { + // let F_i be final formulae + // N_i be non final formula + // (F_1 & ... & F_n & N_1 & ... & N_m) + // = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m) + // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] + formula f = formula::OrRat(std::move(final)); + formula n = formula::AndNLM(std::move(non_final)); + formula t = formula::one_star(); + formula ft = formula::Concat({f, t}); + formula nt = formula::Concat({n, t}); + formula ftn = formula::AndRat({ft, n}); + formula fnt = formula::AndRat({f, nt}); + return formula::OrRat({ftn, fnt}); + } + // No final formula. + // Translate N_1 & N_2 & ... & N_n into + // N_1 && (N_2;[*]) && ... && (N_n;[*]) + // | (N_1;[*]) && N_2 && ... && (N_n;[*]) + // | (N_1;[*]) && (N_2;[*]) && ... && N_n + formula star = formula::one_star(); + std::vector disj; + for (unsigned n = 0; n < s; ++n) + { + std::vector conj; + for (unsigned m = 0; m < s; ++m) + { + formula g = f[m]; + if (n != m) + g = formula::Concat({g, star}); + conj.emplace_back(g); + } + disj.emplace_back(formula::AndRat(std::move(conj))); + } + return formula::OrRat(std::move(disj)); + } + + twa_graph_ptr + derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict, + bool deterministic, derive_opts options) + { + auto aut = make_twa_graph(bdd_dict); + + aut->prop_state_acc(true); + const auto acc_mark = aut->set_buchi(); + + auto formula2state = robin_hood::unordered_map(); + + unsigned init_state = aut->new_state(); + aut->set_init_state(init_state); + + formula2state.insert({ f, init_state }); + + auto f_aps = formula_aps(f); + for (auto& ap : f_aps) + aut->register_ap(ap); + + auto todo = std::vector>(); + todo.push_back({f, init_state}); + + auto state_names = new std::vector(); + std::ostringstream ss; + ss << f; + state_names->push_back(ss.str()); + + auto find_dst = [&](formula derivative) -> unsigned + { + unsigned dst; + auto it = formula2state.find(derivative); + if (it != formula2state.end()) + { + dst = it->second; + } + else + { + dst = aut->new_state(); + todo.push_back({derivative, dst}); + formula2state.insert({derivative, dst}); + std::ostringstream ss; + ss << derivative; + state_names->push_back(ss.str()); + } + + return dst; + }; + + while (!todo.empty()) + { + auto [curr_f, curr_state] = todo[todo.size() - 1]; + todo.pop_back(); + + auto curr_acc_mark = curr_f.accepts_eword() + ? acc_mark + : acc_cond::mark_t(); + + auto [firsts, firsts_support] = first(curr_f, bdd_dict, aut.get()); + for (const bdd one : minterms_of(firsts, firsts_support)) + { + formula derivative = + partial_derivation(curr_f, one, bdd_dict, aut.get(), options); + + // no transition possible from this letter + if (derivative.is(op::ff)) + continue; + + // either the formula isn't an OrRat, or if it is we consider it as + // as a whole to get a deterministic automaton + if (deterministic || !derivative.is(op::OrRat)) + { + auto dst = find_dst(derivative); + aut->new_edge(curr_state, dst, one, curr_acc_mark); + continue; + } + + // formula is an OrRat and we want a non deterministic automaton, + // so consider each child as a destination + for (const auto& subformula : derivative) + { + auto dst = find_dst(subformula); + aut->new_edge(curr_state, dst, one, curr_acc_mark); + } + } + + // if state has no transitions and should be accepting, create + // artificial transition + if (aut->get_graph().state_storage(curr_state).succ == 0 + && curr_f.accepts_eword()) + aut->new_edge(curr_state, curr_state, bddfalse, acc_mark); + } + + aut->set_named_prop("state-names", state_names); + + aut->merge_edges(); + + return aut; + } + + twa_graph_ptr + derive_finite_automaton(formula f, bool deterministic) + { + auto bdd_dict = make_bdd_dict(); + auto aut = make_twa_graph(bdd_dict); + + aut->prop_state_acc(true); + const auto acc_mark = aut->set_buchi(); + + auto formula2state = robin_hood::unordered_map(); + + unsigned init_state = aut->new_state(); + aut->set_init_state(init_state); + + formula2state.insert({ f, init_state }); + + auto f_aps = formula_aps(f); + for (auto& ap : f_aps) + aut->register_ap(ap); + bdd all_aps = aut->ap_vars(); + + auto todo = std::vector>(); + todo.push_back({f, init_state}); + + auto state_names = new std::vector(); + std::ostringstream ss; + ss << f; + state_names->push_back(ss.str()); + + auto find_dst = [&](formula derivative) -> unsigned + { + unsigned dst; + auto it = formula2state.find(derivative); + if (it != formula2state.end()) + { + dst = it->second; + } + else + { + dst = aut->new_state(); + todo.push_back({derivative, dst}); + formula2state.insert({derivative, dst}); + std::ostringstream ss; + ss << derivative; + state_names->push_back(ss.str()); + } + + return dst; + }; + + while (!todo.empty()) + { + auto [curr_f, curr_state] = todo[todo.size() - 1]; + todo.pop_back(); + + auto curr_acc_mark = curr_f.accepts_eword() + ? acc_mark + : acc_cond::mark_t(); + + for (const bdd one : minterms_of(bddtrue, all_aps)) + { + formula derivative = + partial_derivation(curr_f, one, bdd_dict, aut.get()); + + // no transition possible from this letter + if (derivative.is(op::ff)) + continue; + + // either the formula isn't an OrRat, or if it is we consider it as + // as a whole to get a deterministic automaton + if (deterministic || !derivative.is(op::OrRat)) + { + auto dst = find_dst(derivative); + aut->new_edge(curr_state, dst, one, curr_acc_mark); + continue; + } + + // formula is an OrRat and we want a non deterministic automaton, + // so consider each child as a destination + for (const auto& subformula : derivative) + { + auto dst = find_dst(subformula); + aut->new_edge(curr_state, dst, one, curr_acc_mark); + } + } + + // if state has no transitions and should be accepting, create + // artificial transition + if (aut->get_graph().state_storage(curr_state).succ == 0 + && curr_f.accepts_eword()) + aut->new_edge(curr_state, curr_state, bddfalse, acc_mark); + } + + aut->set_named_prop("state-names", state_names); + + aut->merge_edges(); + + return aut; + } + + twa_graph_ptr + derive_automaton_with_first(formula f, bdd_dict_ptr bdd_dict, + bool deterministic) + { + auto finite = derive_finite_automaton_with_first(f, bdd_dict, + deterministic); + + return from_finite(finite); + } + + twa_graph_ptr + derive_automaton(formula f, bool deterministic) + { + auto finite = derive_finite_automaton(f, deterministic); + + return from_finite(finite); + } + + formula + partial_derivation(formula f, const bdd var, const bdd_dict_ptr& d, + void* owner, derive_opts options) + { + if (f.is_boolean()) + { + auto f_bdd = formula_to_bdd(f, d, owner); + + if (bdd_implies(var, f_bdd)) + return formula::eword(); + + return formula::ff(); + } + + switch (f.kind()) + { + // handled by is_boolean above + case op::ff: + case op::tt: + case op::ap: + SPOT_UNREACHABLE(); + + case op::eword: + return formula::ff(); + + // d(E.F) = { d(E).F } U { c(E).d(F) } + case op::Concat: + { + formula E = f[0]; + formula F = f.all_but(0); + + formula d_E = partial_derivation(E, var, d, owner, options); + + formula res; + + if (options.concat_star_distribute && d_E.is(op::OrRat)) + { + std::vector distributed; + for (auto g : d_E) + { + distributed.push_back(formula::Concat({g, F})); + } + + res = formula::OrRat(distributed); + } + else + { + res = + formula::Concat({ partial_derivation(E, var, d, owner, options), F }); + } + + + if (E.accepts_eword()) + res = formula::OrRat( + { res, partial_derivation(F, var, d, owner, options) }); + + return res; + } + + // d(E*) = d(E).E* + // d(E[*i..j]) = d(E).E[*(i-1)..(j-1)] + case op::Star: + { + auto min = f.min() == 0 ? 0 : (f.min() - 1); + auto max = f.max() == formula::unbounded() + ? formula::unbounded() + : (f.max() - 1); + + formula d_E = partial_derivation(f[0], var, d, owner, options); + + if (options.concat_star_distribute && !f[0].is_finite() && d_E.is(op::OrRat)) + { + std::vector distributed; + for (auto g : d_E) + { + distributed.push_back(formula::Concat({g, formula::Star(f[0], min, max)})); + } + + return formula::OrRat(distributed); + } + + return formula::Concat({ d_E, formula::Star(f[0], min, max) }); + } + + // d(E[:*i..j]) = E:E[:*(i-1)..(j-1)] + (eword if i == 0 or c(d(E))) + case op::FStar: + { + formula E = f[0]; + + if (f.min() == 0 && f.max() == 0) + return formula::tt(); + + auto d_E = partial_derivation(E, var, d, owner, options); + + auto min = f.min() == 0 ? 0 : (f.min() - 1); + auto max = f.max() == formula::unbounded() + ? formula::unbounded() + : (f.max() - 1); + + auto results = std::vector(); + + auto E_i_j_minus = formula::FStar(E, min, max); + results.push_back(formula::Fusion({ d_E, E_i_j_minus })); + + if (d_E.accepts_eword()) + results.push_back(d_E); + + if (f.min() == 0) + results.push_back(formula::eword()); + + return formula::OrRat(std::move(results)); + } + + // d(E && F) = d(E) && d(F) + // d(E + F) = {d(E)} U {d(F)} + case op::AndRat: + case op::OrRat: + { + std::vector subderivations; + for (auto subformula : f) + { + auto subderivation = + partial_derivation(subformula, var, d, owner, options); + subderivations.push_back(subderivation); + } + return formula::multop(f.kind(), std::move(subderivations)); + } + + case op::AndNLM: + { + formula rewrite = rewrite_and_nlm(f); + return partial_derivation(rewrite, var, d, owner, options); + } + + // d(E:F) = {d(E):F} U {c(d(E)).d(F)} + case op::Fusion: + { + formula E = f[0]; + formula F = f.all_but(0); + + auto d_E = partial_derivation(E, var, d, owner, options); + auto res = formula::Fusion({ d_E, F }); + + if (d_E.accepts_eword()) + res = + formula::OrRat({ res, partial_derivation(F, var, d, owner, options) }); + + return res; + } + + case op::first_match: + { + formula E = f[0]; + auto d_E = partial_derivation(E, var, d, owner, options); + // if d_E.accepts_eword(), first_match(d_E) will return eword + return formula::first_match(d_E); + } + + default: + std::cerr << "unimplemented kind " + << static_cast(f.kind()) + << std::endl; + SPOT_UNIMPLEMENTED(); + } + return formula::ff(); + } +} diff --git a/spot/tl/derive.hh b/spot/tl/derive.hh new file mode 100644 index 000000000..993db2ed2 --- /dev/null +++ b/spot/tl/derive.hh @@ -0,0 +1,60 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// 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 . + +#pragma once + +#include + +#include + +#include +#include +#include + +namespace spot +{ + + struct derive_opts + { + bool concat_star_distribute = true; + }; + + /// \ingroup tl_misc + /// \brief Produce a SERE formula's partial derivative + SPOT_API formula + partial_derivation(formula f, const bdd var, const bdd_dict_ptr& d, + void* owner, derive_opts options = {}); + + SPOT_API twa_graph_ptr + derive_automaton(formula f, bool deterministic = true); + + SPOT_API twa_graph_ptr + derive_automaton_with_first(formula f, bdd_dict_ptr bdd_dict, + bool deterministic = true); + + SPOT_API twa_graph_ptr + derive_finite_automaton(formula f, bool deterministic = true); + + SPOT_API twa_graph_ptr + derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict, + bool deterministic = true, derive_opts options = {}); + + SPOT_API formula + rewrite_and_nlm(formula f); +} diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc new file mode 100644 index 000000000..402236ea6 --- /dev/null +++ b/spot/tl/expansions.cc @@ -0,0 +1,966 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// 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 "config.h" +#include +#include +#include +#include +#include +#include +#include +#include + +namespace spot +{ + namespace + { + // FIXME: could probably just return a map directly + static std::vector + formula_aps(formula f) + { + auto res = std::unordered_set(); + + f.traverse([&res](formula f) + { + if (f.is(op::ap)) + { + res.insert(f.ap_name()); + return true; + } + + return false; + }); + + return std::vector(res.begin(), res.end()); + } + + formula + rewrite_and_nlm(formula f) + { + unsigned s = f.size(); + std::vector final; + std::vector non_final; + + for (auto g: f) + if (g.accepts_eword()) + final.emplace_back(g); + else + non_final.emplace_back(g); + + if (non_final.empty()) + // (a* & b*);c = (a*|b*);c + return formula::OrRat(std::move(final)); + if (!final.empty()) + { + // let F_i be final formulae + // N_i be non final formula + // (F_1 & ... & F_n & N_1 & ... & N_m) + // = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m) + // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] + formula f = formula::OrRat(std::move(final)); + formula n = formula::AndNLM(std::move(non_final)); + formula t = formula::one_star(); + formula ft = formula::Concat({f, t}); + formula nt = formula::Concat({n, t}); + formula ftn = formula::AndRat({ft, n}); + formula fnt = formula::AndRat({f, nt}); + return formula::OrRat({ftn, fnt}); + } + // No final formula. + // Translate N_1 & N_2 & ... & N_n into + // N_1 && (N_2;[*]) && ... && (N_n;[*]) + // | (N_1;[*]) && N_2 && ... && (N_n;[*]) + // | (N_1;[*]) && (N_2;[*]) && ... && N_n + formula star = formula::one_star(); + std::vector disj; + for (unsigned n = 0; n < s; ++n) + { + std::vector conj; + for (unsigned m = 0; m < s; ++m) + { + formula g = f[m]; + if (n != m) + g = formula::Concat({g, star}); + conj.emplace_back(g); + } + disj.emplace_back(formula::AndRat(std::move(conj))); + } + return formula::OrRat(std::move(disj)); + } + + class bdd_finalizer + { + public: + int encode(formula f) + { + bool is_anon = false; + int var_num; + auto it = formula2bdd_.find(f); + if (it != formula2bdd_.end()) + { + var_num = it->second; + } + else + { + if (opt_sigma_star_ && (f.is(op::Star) + && f[0].is(op::tt) + && f.min() == 0 + && f.max() == formula::unbounded())) + { + var_num = bddtrue.id(); + } + else if (opt_bdd_encode_ && (f.is(op::AndRat) || f.is(op::OrRat))) + { + bdd var = f.is(op::AndRat) ? bdd(bddtrue) : bdd(bddfalse); + for (const auto& sub_f : f) + { + int bddid = encode(sub_f); + bdd subvar = bdd_ithvar(bddid); + var = f.is(op::AndRat) ? var & subvar : var | subvar; + } + var_num = var.id(); + } + else + { + var_num = d_->register_anonymous_variables(1, this); + is_anon = true; + } + + formula2bdd_.insert({f, var_num}); + bdd2formula_.insert({var_num, f}); + } + + bdd var = bdd_ithvar(var_num); + + if (is_anon) + anon_set_ &= var; + + return var_num; + } + + bdd_finalizer(expansion_t& exp, bdd_dict_ptr d, bool opt_sigma_star, bool opt_bdd_encode) + : anon_set_(bddtrue) + , d_(d) + , opt_sigma_star_(opt_sigma_star) + , opt_bdd_encode_(opt_bdd_encode) + { + for (const auto& [prefix, suffix] : exp) + { + int var_num = encode(suffix); + bdd var = bdd_ithvar(var_num); + exp_ |= prefix & var; + } + } + + ~bdd_finalizer() + { + d_->unregister_all_my_variables(this); + } + + expansion_t + simplify(exp_opts::expand_opt opts); + + private: + bdd exp_; + bdd anon_set_; + std::map formula2bdd_; + std::map bdd2formula_; + bdd_dict_ptr d_; + bool opt_sigma_star_; + bool opt_bdd_encode_; + + formula var_to_formula(int var); + formula conj_bdd_to_sere(bdd b); + formula bdd_to_sere(bdd b); + }; + + formula + bdd_finalizer::var_to_formula(int var) + { + formula f = bdd2formula_[var]; + assert(f); + return f; + } + + formula + bdd_finalizer::bdd_to_sere(bdd f) + { + if (f == bddfalse) + return formula::ff(); + + std::vector v; + minato_isop isop(f); + bdd cube; + while ((cube = isop.next()) != bddfalse) + v.emplace_back(conj_bdd_to_sere(cube)); + return formula::OrRat(std::move(v)); + } + + formula + bdd_finalizer::conj_bdd_to_sere(bdd b) + { + if (b == bddtrue) + { + if (opt_sigma_star_){ + return formula::Star(formula::tt(), 0, formula::unbounded()); + } else { + return formula::tt(); + } + } + if (b == bddfalse) + return formula::ff(); + + // Unroll the first loop of the next do/while loop so that we + // do not have to create v when b is not a conjunction. + formula res = var_to_formula(bdd_var(b)); + bdd high = bdd_high(b); + if (high == bddfalse) + { + res = formula::Not(res); + b = bdd_low(b); + } + else + { + assert(bdd_low(b) == bddfalse); + b = high; + } + if (b == bddtrue) + return res; + std::vector v{std::move(res)}; + do + { + res = var_to_formula(bdd_var(b)); + high = bdd_high(b); + if (high == bddfalse) + { + res = formula::Not(res); + b = bdd_low(b); + } + else + { + assert(bdd_low(b) == bddfalse); + b = high; + } + assert(b != bddfalse); + v.emplace_back(std::move(res)); + } + while (b != bddtrue); + return formula::multop(op::AndRat, std::move(v)); + } + + expansion_t + bdd_finalizer::simplify(exp_opts::expand_opt opts) + { + expansion_t res; + + if (opts & exp_opts::expand_opt::BddMinterm) + { + bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_); + bdd or_labels = bdd_exist(exp_, anon_set_); + // TODO: check are_equivalent avec or_labels/exp_ en premier argument + for (bdd letter: minterms_of(or_labels, prop_set)) + { + bdd dest_bdd = bdd_restrict(exp_, letter); + formula dest = bdd_to_sere(dest_bdd); + + // #ifndef NDEBUG + // // make sure it didn't exist before + // auto it = std::find(res.begin(), res.end(), {letter, dest}); + // SPOT_ASSERT(it == res.end()); + // #endif + + res.push_back({letter, dest}); + } + } + else // BddIsop + { + minato_isop isop(exp_); + bdd cube; + while ((cube = isop.next()) != bddfalse) + { + bdd letter = bdd_exist(cube, anon_set_); + bdd suffix = bdd_existcomp(cube, anon_set_); + formula dest = conj_bdd_to_sere(suffix); + + res.push_back({letter, dest}); + } + } + + return res; + } + + expansion_t + unique_prefix(const expansion_t& exp) + { + std::map unique_map; + for (const auto& [prefix, suffix] : exp) + { + auto res = unique_map.insert({prefix, suffix}); + if (!res.second) + { + auto it = res.first; + it->second = formula::OrRat({it->second, suffix}); + } + } + + expansion_t res(unique_map.begin(), unique_map.end()); + return res; + } + + expansion_t + unique_prefix_seen(const expansion_t& exp, std::unordered_set* seen) + { + std::map unique_map; + for (const auto& [prefix, suffix] : exp) + { + auto res = unique_map.insert({prefix, suffix}); + if (!res.second) + { + auto it = res.first; + it->second = formula::OrRat({it->second, suffix}); + } + } + + expansion_t res; + + for (const auto& [prefix, suffix] : unique_map) + { + if (!suffix.is(op::OrRat)) + { + res.push_back({prefix, suffix}); + continue; + } + + std::vector merge; + std::vector single; + + for (const auto& sub_f : suffix) + { + if (seen->find(sub_f) != seen->end()) + { + single.push_back(sub_f); + } + else + { + merge.push_back(sub_f); + } + } + + for (const auto& sub_f : single) + res.push_back({prefix, sub_f}); + + if (!merge.empty()) + res.push_back({prefix, formula::OrRat(merge)}); + } + + return res; + } + + size_t count_new(const expansion_t& exp, std::unordered_set* seen) + { + size_t count = 0; + for (const auto& [_, suffix] : exp) + { + if (seen->find(suffix) == seen->end()) + count++; + } + return count; + } + + const expansion_t& + find_smallest(const expansion_t& left, + const expansion_t& right, + std::unordered_set* seen) + { + size_t left_new = count_new(left, seen); + size_t right_new = count_new(right, seen); + + if (left_new < right_new) + return left; + + if (left_new == right_new && left.size() > right.size()) + return right; + + return right; + } + + expansion_t + unique_prefix_count(const expansion_t& exp, std::unordered_set* seen) + { + expansion_t up = unique_prefix(exp); + expansion_t up_seen = unique_prefix_seen(exp, seen); + + const expansion_t& maybe_smallest = find_smallest(exp, up, seen); + const expansion_t& smallest = find_smallest(maybe_smallest, up_seen, seen); + + return smallest; + } + + void + finalize(expansion_t& exp, exp_opts::expand_opt opts, bdd_dict_ptr d, std::unordered_set* seen) + { + if (opts & (exp_opts::expand_opt::BddIsop + | exp_opts::expand_opt::BddMinterm)) + { + bdd_finalizer bddf(exp, d, opts & exp_opts::expand_opt::BddSigmaStar, opts & exp_opts::expand_opt::BddEncode); + exp = bddf.simplify(opts); + } + + if (opts & exp_opts::expand_opt::UniqueSuffixPre) + { + std::map unique_map; + for (const auto& [prefix, suffix] : exp) + { + auto res = unique_map.insert({suffix, prefix}); + if (!res.second) + { + auto it = res.first; + it->second |= prefix; + } + } + + exp.clear(); + for (const auto& [suffix, prefix] : unique_map) + { + exp.push_back({prefix, suffix}); + } + } + + if (opts & exp_opts::expand_opt::UniquePrefix + || opts & exp_opts::expand_opt::UniquePrefixSeenOpt + || opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt) + { + if (opts & exp_opts::expand_opt::UniquePrefixSeenOpt) + exp = unique_prefix_seen(exp, seen); + else if (opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt) + exp = unique_prefix_count(exp, seen); + else + exp = unique_prefix(exp); + } + + if (opts & exp_opts::expand_opt::UniqueSuffixPost) + { + std::map unique_map; + for (const auto& [prefix, suffix] : exp) + { + auto res = unique_map.insert({suffix, prefix}); + if (!res.second) + { + auto it = res.first; + it->second |= prefix; + } + } + + exp.clear(); + for (const auto& [suffix, prefix] : unique_map) + { + exp.push_back({prefix, suffix}); + } + } + + if (opts & exp_opts::expand_opt::Determinize) + { + expansion_t exp_new; + + bdd props = bddtrue; + for (const auto& [prefix, _] : exp) + props &= bdd_support(prefix); + + std::vector dests; + for (bdd letter : minterms_of(bddtrue, props)) + { + for (const auto& [prefix, suffix] : exp) + { + if (bdd_implies(letter, prefix)) + dests.push_back(suffix); + } + formula or_dests = formula::OrRat(dests); + exp_new.push_back({letter, or_dests}); + dests.clear(); + } + exp = exp_new; + } + + // sort and remove duplicates from expansion to canonicalize it for + // eventual signature use + if (exp.size() >= 2) + { + std::sort(exp.begin(), exp.end(), + [](const auto& lhs, const auto& rhs) { + return std::make_pair(lhs.first.id(), lhs.second.id()) + < std::make_pair(rhs.first.id(), rhs.second.id()); + }); + exp.erase(std::unique(exp.begin(), exp.end()), exp.end()); + } + } + } + + formula + expansion_to_formula(expansion_t e, bdd_dict_ptr& d) + { + std::vector res; + + for (const auto& [key, val] : e) + { + formula prefix = bdd_to_formula(key, d); + res.push_back(formula::Concat({prefix, val})); + } + + return formula::OrRat(res); + } + + void print_expansion(const expansion_t& exp, const bdd_dict_ptr& dict) + { + for (const auto& [prefix, suffix] : exp) + { + std::cout << bdd_to_formula(prefix, dict) << ": " << suffix << std::endl; + } + } + + std::vector> + expansion_simple(formula f) + { + int owner = 42; + auto d = make_bdd_dict(); + + auto exp = expansion(f, d, &owner, exp_opts::None); + + std::vector> res; + for (const auto& [bdd, f] : exp) + res.push_back({bdd_to_formula(bdd, d), f}); + + d->unregister_all_my_variables(&owner); + return res; + } + + expansion_t + expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set* seen) + { + using exp_t = expansion_t; + + if (f.is_boolean()) + { + auto f_bdd = formula_to_bdd(f, d, owner); + + if (f_bdd == bddfalse) + return {}; + + return {{f_bdd, formula::eword()}}; + } + + auto rec = [&d, owner, seen](formula f){ + return expansion(f, d, owner, exp_opts::None, seen); + }; + + + switch (f.kind()) + { + case op::ff: + case op::tt: + case op::ap: + SPOT_UNREACHABLE(); + + case op::eword: + // return {{bddfalse, formula::ff()}}; + return {}; + + case op::Concat: + { + auto exps = rec(f[0]); + + exp_t res; + for (const auto& [bdd_l, form] : exps) + { + res.push_back({bdd_l, formula::Concat({form, f.all_but(0)})}); + } + + if (f[0].accepts_eword()) + { + auto exps_rest = rec(f.all_but(0)); + for (const auto& [bdd_l, form] : exps_rest) + { + res.push_back({bdd_l, form}); + } + } + + finalize(res, opts, d, seen); + return res; + } + + case op::FStar: + { + formula E = f[0]; + + if (f.min() == 0 && f.max() == 0) + return {{bddtrue, formula::eword()}}; + + auto min = f.min() == 0 ? 0 : (f.min() - 1); + auto max = f.max() == formula::unbounded() + ? formula::unbounded() + : (f.max() - 1); + + auto E_i_j_minus = formula::FStar(E, min, max); + + auto exp = rec(E); + exp_t res; + for (const auto& [li, ei] : exp) + { + res.push_back({li, formula::Fusion({ei, E_i_j_minus})}); + + if (ei.accepts_eword() && f.min() != 0) + { + for (const auto& [ki, fi] : rec(E_i_j_minus)) + { + // FIXME: build bdd once + if ((li & ki) != bddfalse) + res.push_back({li & ki, fi}); + } + } + } + if (f.min() == 0) + res.push_back({bddtrue, formula::eword()}); + + finalize(res, opts, d, seen); + return res; + } + + case op::Star: + { + auto min = f.min() == 0 ? 0 : (f.min() - 1); + auto max = f.max() == formula::unbounded() + ? formula::unbounded() + : (f.max() - 1); + + auto exps = rec(f[0]); + + exp_t res; + for (const auto& [bdd_l, form] : exps) + { + res.push_back({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})}); + } + + finalize(res, opts, d, seen); + return res; + } + + case op::AndNLM: + { + formula rewrite = rewrite_and_nlm(f); + auto res = rec(rewrite); + finalize(res, opts, d, seen); + return res; + } + + case op::first_match: + { + auto exps = rec(f[0]); + + exp_t res; + for (const auto& [bdd_l, form] : exps) + { + res.push_back({bdd_l, form}); + } + + // determinize + bdd or_labels = bddfalse; + bdd support = bddtrue; + bool is_det = true; + for (const auto& [l, _] : res) + { + support &= bdd_support(l); + if (is_det) + is_det = !bdd_have_common_assignment(l, or_labels); + or_labels |= l; + } + + if (is_det) + { + for (auto& [_, dest] : res) + dest = formula::first_match(dest); + finalize(res, opts, d, seen); + return res; + } + + exp_t res_det; + std::vector dests; + for (bdd l: minterms_of(or_labels, support)) + { + for (const auto& [ndet_label, ndet_dest] : res) + { + if (bdd_implies(l, ndet_label)) + dests.push_back(ndet_dest); + } + formula or_dests = formula::OrRat(dests); + res_det.push_back({l, or_dests}); + dests.clear(); + } + + for (auto& [_, dest] : res_det) + dest = formula::first_match(dest); + finalize(res_det, opts, d, seen); + return res_det; + } + + case op::Fusion: + { + exp_t res; + formula E = f[0]; + formula F = f.all_but(0); + + exp_t Ei = rec(E); + // TODO: std::option + exp_t Fj = rec(F); + + for (const auto& [li, ei] : Ei) + { + if (ei.accepts_eword()) + { + for (const auto& [kj, fj] : Fj) + if ((li & kj) != bddfalse) + res.push_back({li & kj, fj}); + } + + formula ei_fusion_F = formula::Fusion({ei, F}); + if (!ei_fusion_F.is(op::ff)) + res.push_back({li, ei_fusion_F}); + } + + finalize(res, opts, d, seen); + return res; + } + + case op::AndRat: + { + exp_t res; + for (const auto& sub_f : f) + { + auto exps = rec(sub_f); + + if (exps.empty()) + { + // op::AndRat: one of the expansions was empty (the only + // edge was `false`), so the AndRat is empty as + // well + res.clear(); + break; + } + + if (res.empty()) + { + res = std::move(exps); + continue; + } + + exp_t new_res; + bool inserted = false; + for (const auto& [l_key, l_val] : exps) + { + for (const auto& [r_key, r_val] : res) + { + if ((l_key & r_key) != bddfalse) + { + new_res.push_back({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})}); + inserted = true; + } + } + } + + if (!inserted) + { + // all prefix conjuctions led to bddfalse, And is empty + res.clear(); + break; + } + + res = std::move(new_res); + } + + finalize(res, opts, d, seen); + return res; + } + + case op::OrRat: + { + exp_t res; + for (const auto& sub_f : f) + { + auto exps = rec(sub_f); + if (exps.empty()) + continue; + + if (res.empty()) + { + res = std::move(exps); + continue; + } + + for (const auto& [label, dest] : exps) + res.push_back({label, dest}); + } + + finalize(res, opts, d, seen); + return res; + } + + default: + std::cerr << "unimplemented kind " + << static_cast(f.kind()) + << std::endl; + SPOT_UNIMPLEMENTED(); + } + + return {}; + } + + twa_graph_ptr + expand_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts) + { + auto finite = expand_finite_automaton(f, d, opts); + return from_finite(finite); + } + + struct signature_hash + { + std::size_t + operator() (const std::pair& sig) const noexcept + { + size_t hash = std::hash()(sig.first); + + for (const auto& keyvalue : sig.second) + { + hash ^= (bdd_hash()(keyvalue.first) ^ std::hash()(keyvalue.second)) + + 0x9e3779b9 + (hash << 6) + (hash >> 2); + } + + return hash; + } + }; + + twa_graph_ptr + expand_finite_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts) + { + bool signature_merge = opts & exp_opts::expand_opt::SignatureMerge; + + auto aut = make_twa_graph(d); + + aut->prop_state_acc(true); + const auto acc_mark = aut->set_buchi(); + + auto formula2state = robin_hood::unordered_map(); + auto signature2state = std::unordered_map, unsigned, signature_hash>(); + auto seen = std::unordered_set(); + seen.insert(f); + + unsigned init_state = aut->new_state(); + aut->set_init_state(init_state); + formula2state.insert({ f, init_state }); + + + auto f_aps = formula_aps(f); + for (auto& ap : f_aps) + aut->register_ap(ap); + + if (signature_merge) + signature2state.insert({ {f.accepts_eword(), expansion(f, d, aut.get(), opts, &seen)}, init_state}); + + + auto todo = std::vector>(); + todo.push_back({f, init_state}); + + auto state_names = new std::vector(); + std::ostringstream ss; + ss << f; + state_names->push_back(ss.str()); + + auto find_dst = [&](formula suffix) -> unsigned + { + unsigned dst; + auto it = formula2state.find(suffix); + if (it != formula2state.end()) + { + dst = it->second; + } + else + { + if (signature_merge) + { + auto exp = expansion(suffix, d, aut.get(), opts, &seen); + bool accepting = suffix.accepts_eword(); + auto it2 = signature2state.find({accepting, exp}); + if (it2 != signature2state.end()) + { + formula2state.insert({suffix, it2->second}); + return it2->second; + } + } + + dst = aut->new_state(); + todo.push_back({suffix, dst}); + seen.insert(suffix); + + formula2state.insert({suffix, dst}); + if (signature_merge) + signature2state.insert({{suffix.accepts_eword(), expansion(suffix, d, aut.get(), opts, &seen)}, dst}); + + std::ostringstream ss; + ss << suffix; + state_names->push_back(ss.str()); + } + + return dst; + }; + + while (!todo.empty()) + { + auto [curr_f, curr_state] = todo[todo.size() - 1]; + todo.pop_back(); + + auto curr_acc_mark= curr_f.accepts_eword() + ? acc_mark + : acc_cond::mark_t(); + + auto exp = expansion(curr_f, d, aut.get(), opts, &seen); + + for (const auto& [letter, suffix] : exp) + { + if (suffix.is(op::ff)) + // TODO ASSERT NOT + continue; + + auto dst = find_dst(suffix); + aut->new_edge(curr_state, dst, letter, curr_acc_mark); + } + + // if state has no transitions and should be accepting, create + // artificial transition + if (aut->get_graph().state_storage(curr_state).succ == 0 + && curr_f.accepts_eword()) + aut->new_edge(curr_state, curr_state, bddfalse, acc_mark); + } + + aut->set_named_prop("state-names", state_names); + + if ((opts & exp_opts::MergeEdges) + && !(opts & exp_opts::UniqueSuffixPre || opts & exp_opts::UniqueSuffixPost)) + aut->merge_edges(); + + return aut; + } +} diff --git a/spot/tl/expansions.hh b/spot/tl/expansions.hh new file mode 100644 index 000000000..9db8d2c8d --- /dev/null +++ b/spot/tl/expansions.hh @@ -0,0 +1,72 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// 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 . + +#pragma once + +#include + +#include + +#include +#include +#include +#include + +namespace spot +{ + using expansion_t = std::vector>; + + struct exp_opts + { + enum expand_opt { + None = 0, + UniqueSuffixPre = 1, + UniquePrefix = 2, + BddIsop = 4, + BddMinterm = 8, + BddSigmaStar = 16, + BddEncode = 32, + MergeEdges = 64, + SignatureMerge = 128, + Determinize = 256, + UniquePrefixSeenOpt = 512, + UniqueSuffixPost = 1024, + UniquePrefixSeenCountOpt = 2048, + TransitionBased = 4096, + }; + }; + + SPOT_API std::vector> + expansion_simple(formula f); + + SPOT_API expansion_t + expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set* seen = nullptr); + + SPOT_API twa_graph_ptr + expand_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts); + + SPOT_API twa_graph_ptr + expand_finite_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts); + + SPOT_API formula + expansion_to_formula(expansion_t e, bdd_dict_ptr& d); + + SPOT_API void + print_expansion(const expansion_t& exp, const bdd_dict_ptr& dict); +} diff --git a/spot/tl/expansions2.cc b/spot/tl/expansions2.cc new file mode 100644 index 000000000..c40298d7f --- /dev/null +++ b/spot/tl/expansions2.cc @@ -0,0 +1,946 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// 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 "config.h" +#include +#include +#include +#include +#include +#include +#include +#include + +namespace spot +{ + namespace + { + // FIXME: could probably just return a map directly + static std::vector + formula_aps(formula f) + { + auto res = std::unordered_set(); + + f.traverse([&res](formula f) + { + if (f.is(op::ap)) + { + res.insert(f.ap_name()); + return true; + } + + return false; + }); + + return std::vector(res.begin(), res.end()); + } + + formula + rewrite_and_nlm(formula f) + { + unsigned s = f.size(); + std::vector final; + std::vector non_final; + + for (auto g: f) + if (g.accepts_eword()) + final.emplace_back(g); + else + non_final.emplace_back(g); + + if (non_final.empty()) + // (a* & b*);c = (a*|b*);c + return formula::OrRat(std::move(final)); + if (!final.empty()) + { + // let F_i be final formulae + // N_i be non final formula + // (F_1 & ... & F_n & N_1 & ... & N_m) + // = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m) + // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] + formula f = formula::OrRat(std::move(final)); + formula n = formula::AndNLM(std::move(non_final)); + formula t = formula::one_star(); + formula ft = formula::Concat({f, t}); + formula nt = formula::Concat({n, t}); + formula ftn = formula::AndRat({ft, n}); + formula fnt = formula::AndRat({f, nt}); + return formula::OrRat({ftn, fnt}); + } + // No final formula. + // Translate N_1 & N_2 & ... & N_n into + // N_1 && (N_2;[*]) && ... && (N_n;[*]) + // | (N_1;[*]) && N_2 && ... && (N_n;[*]) + // | (N_1;[*]) && (N_2;[*]) && ... && N_n + formula star = formula::one_star(); + std::vector disj; + for (unsigned n = 0; n < s; ++n) + { + std::vector conj; + for (unsigned m = 0; m < s; ++m) + { + formula g = f[m]; + if (n != m) + g = formula::Concat({g, star}); + conj.emplace_back(g); + } + disj.emplace_back(formula::AndRat(std::move(conj))); + } + return formula::OrRat(std::move(disj)); + } + + class bdd_finalizer + { + public: + int encode(formula f) + { + bool is_anon = false; + int var_num; + auto it = formula2bdd_.find(f); + if (it != formula2bdd_.end()) + { + var_num = it->second; + } + else + { + if (opt_sigma_star_ && (f.is(op::Star) + && f[0].is(op::tt) + && f.min() == 0 + && f.max() == formula::unbounded())) + { + var_num = bddtrue.id(); + } + else if (opt_bdd_encode_ && (f.is(op::AndRat) || f.is(op::OrRat))) + { + bdd var = f.is(op::AndRat) ? bdd(bddtrue) : bdd(bddfalse); + for (const auto& sub_f : f) + { + int bddid = encode(sub_f); + bdd subvar = bdd_ithvar(bddid); + var = f.is(op::AndRat) ? var & subvar : var | subvar; + } + var_num = var.id(); + } + else + { + var_num = d_->register_anonymous_variables(1, this); + is_anon = true; + } + + formula2bdd_.insert({f, var_num}); + bdd2formula_.insert({var_num, f}); + } + + bdd var = bdd_ithvar(var_num); + + if (is_anon) + anon_set_ &= var; + + return var_num; + } + + bdd_finalizer(expansion_t& exp, bdd_dict_ptr d, bool opt_sigma_star, bool opt_bdd_encode) + : anon_set_(bddtrue) + , d_(d) + , opt_sigma_star_(opt_sigma_star) + , opt_bdd_encode_(opt_bdd_encode) + { + for (const auto& [prefix, suffix] : exp) + { + int var_num = encode(suffix); + bdd var = bdd_ithvar(var_num); + exp_ |= prefix & var; + } + } + + ~bdd_finalizer() + { + d_->unregister_all_my_variables(this); + } + + expansion_t + simplify(exp_opts::expand_opt opts); + + private: + bdd exp_; + bdd anon_set_; + std::map formula2bdd_; + std::map bdd2formula_; + bdd_dict_ptr d_; + bool opt_sigma_star_; + bool opt_bdd_encode_; + + formula var_to_formula(int var); + formula conj_bdd_to_sere(bdd b); + formula bdd_to_sere(bdd b); + }; + + formula + bdd_finalizer::var_to_formula(int var) + { + formula f = bdd2formula_[var]; + assert(f); + return f; + } + + formula + bdd_finalizer::bdd_to_sere(bdd f) + { + if (f == bddfalse) + return formula::ff(); + + std::vector v; + minato_isop isop(f); + bdd cube; + while ((cube = isop.next()) != bddfalse) + v.emplace_back(conj_bdd_to_sere(cube)); + return formula::OrRat(std::move(v)); + } + + formula + bdd_finalizer::conj_bdd_to_sere(bdd b) + { + if (b == bddtrue) + { + if (opt_sigma_star_){ + return formula::Star(formula::tt(), 0, formula::unbounded()); + } else { + return formula::tt(); + } + } + if (b == bddfalse) + return formula::ff(); + + // Unroll the first loop of the next do/while loop so that we + // do not have to create v when b is not a conjunction. + formula res = var_to_formula(bdd_var(b)); + bdd high = bdd_high(b); + if (high == bddfalse) + { + res = formula::Not(res); + b = bdd_low(b); + } + else + { + assert(bdd_low(b) == bddfalse); + b = high; + } + if (b == bddtrue) + return res; + std::vector v{std::move(res)}; + do + { + res = var_to_formula(bdd_var(b)); + high = bdd_high(b); + if (high == bddfalse) + { + res = formula::Not(res); + b = bdd_low(b); + } + else + { + assert(bdd_low(b) == bddfalse); + b = high; + } + assert(b != bddfalse); + v.emplace_back(std::move(res)); + } + while (b != bddtrue); + return formula::multop(op::AndRat, std::move(v)); + } + + expansion_t + bdd_finalizer::simplify(exp_opts::expand_opt opts) + { + expansion_t res; + + if (opts & exp_opts::expand_opt::BddMinterm) + { + bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_); + bdd or_labels = bdd_exist(exp_, anon_set_); + // TODO: check are_equivalent avec or_labels/exp_ en premier argument + for (bdd letter: minterms_of(or_labels, prop_set)) + { + bdd dest_bdd = bdd_restrict(exp_, letter); + formula dest = bdd_to_sere(dest_bdd); + + // #ifndef NDEBUG + // // make sure it didn't exist before + // auto it = std::find(res.begin(), res.end(), {letter, dest}); + // SPOT_ASSERT(it == res.end()); + // #endif + + res.push_back({letter, dest}); + } + } + else // BddIsop + { + minato_isop isop(exp_); + bdd cube; + while ((cube = isop.next()) != bddfalse) + { + bdd letter = bdd_exist(cube, anon_set_); + bdd suffix = bdd_existcomp(cube, anon_set_); + formula dest = conj_bdd_to_sere(suffix); + + res.push_back({letter, dest}); + } + } + + return res; + } + + expansion_t + unique_prefix(const expansion_t& exp) + { + std::map unique_map; + for (const auto& [prefix, suffix] : exp) + { + auto res = unique_map.insert({prefix, suffix}); + if (!res.second) + { + auto it = res.first; + it->second = formula::OrRat({it->second, suffix}); + } + } + + expansion_t res(unique_map.begin(), unique_map.end()); + return res; + } + + expansion_t + unique_prefix_seen(const expansion_t& exp, std::unordered_set* seen) + { + std::map unique_map; + for (const auto& [prefix, suffix] : exp) + { + auto res = unique_map.insert({prefix, suffix}); + if (!res.second) + { + auto it = res.first; + it->second = formula::OrRat({it->second, suffix}); + } + } + + expansion_t res; + + for (const auto& [prefix, suffix] : unique_map) + { + if (!suffix.is(op::OrRat)) + { + res.push_back({prefix, suffix}); + continue; + } + + std::vector merge; + std::vector single; + + for (const auto& sub_f : suffix) + { + if (seen->find(sub_f) != seen->end()) + { + single.push_back(sub_f); + } + else + { + merge.push_back(sub_f); + } + } + + for (const auto& sub_f : single) + res.push_back({prefix, sub_f}); + + if (!merge.empty()) + res.push_back({prefix, formula::OrRat(merge)}); + } + + return res; + } + + size_t count_new(const expansion_t& exp, std::unordered_set* seen) + { + size_t count = 0; + for (const auto& [_, suffix] : exp) + { + if (seen->find(suffix) == seen->end()) + count++; + } + return count; + } + + const expansion_t& + find_smallest(const expansion_t& left, + const expansion_t& right, + std::unordered_set* seen) + { + size_t left_new = count_new(left, seen); + size_t right_new = count_new(right, seen); + + if (left_new < right_new) + return left; + + if (left_new == right_new && left.size() > right.size()) + return right; + + return right; + } + + expansion_t + unique_prefix_count(const expansion_t& exp, std::unordered_set* seen) + { + expansion_t up = unique_prefix(exp); + expansion_t up_seen = unique_prefix_seen(exp, seen); + + const expansion_t& maybe_smallest = find_smallest(exp, up, seen); + const expansion_t& smallest = find_smallest(maybe_smallest, up_seen, seen); + + return smallest; + } + + void + finalize(expansion_t& exp, exp_opts::expand_opt opts, bdd_dict_ptr d, std::unordered_set* seen) + { + if (opts & (exp_opts::expand_opt::BddIsop + | exp_opts::expand_opt::BddMinterm)) + { + bdd_finalizer bddf(exp, d, opts & exp_opts::expand_opt::BddSigmaStar, opts & exp_opts::expand_opt::BddEncode); + exp = bddf.simplify(opts); + } + + if (opts & exp_opts::expand_opt::UniqueSuffixPre) + { + std::map unique_map; + for (const auto& [prefix, suffix] : exp) + { + auto res = unique_map.insert({suffix, prefix}); + if (!res.second) + { + auto it = res.first; + it->second |= prefix; + } + } + + exp.clear(); + for (const auto& [suffix, prefix] : unique_map) + { + exp.push_back({prefix, suffix}); + } + } + + if (opts & exp_opts::expand_opt::UniquePrefix + || opts & exp_opts::expand_opt::UniquePrefixSeenOpt + || opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt) + { + if (opts & exp_opts::expand_opt::UniquePrefixSeenOpt) + exp = unique_prefix_seen(exp, seen); + else if (opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt) + exp = unique_prefix_count(exp, seen); + else + exp = unique_prefix(exp); + } + + if (opts & exp_opts::expand_opt::UniqueSuffixPost) + { + std::map unique_map; + for (const auto& [prefix, suffix] : exp) + { + auto res = unique_map.insert({suffix, prefix}); + if (!res.second) + { + auto it = res.first; + it->second |= prefix; + } + } + + exp.clear(); + for (const auto& [suffix, prefix] : unique_map) + { + exp.push_back({prefix, suffix}); + } + } + + if (opts & exp_opts::expand_opt::Determinize) + { + expansion_t exp_new; + + bdd props = bddtrue; + for (const auto& [prefix, _] : exp) + props &= bdd_support(prefix); + + std::vector dests; + for (bdd letter : minterms_of(bddtrue, props)) + { + for (const auto& [prefix, suffix] : exp) + { + if (bdd_implies(letter, prefix)) + dests.push_back(suffix); + } + formula or_dests = formula::OrRat(dests); + exp_new.push_back({letter, or_dests}); + dests.clear(); + } + exp = exp_new; + } + + // sort expansion to canonicalize it for eventual signature use + if (exp.size() >= 2) + { + std::sort(exp.begin(), exp.end(), + [](const auto& lhs, const auto& rhs) { + return std::make_pair(lhs.first.id(), lhs.second.id()) + < std::make_pair(rhs.first.id(), rhs.second.id()); + }); + exp.erase(std::unique(exp.begin(), exp.end()), exp.end()); + } + } + } + + formula + expansion_to_formula2(expansion_t e, bdd_dict_ptr& d) + { + std::vector res; + + for (const auto& [key, val] : e) + { + formula prefix = bdd_to_formula(key, d); + res.push_back(formula::Concat({prefix, val})); + } + + return formula::OrRat(res); + } + + expansion_t + expansion2(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set* seen) + { + using exp_t = expansion_t; + + if (f.is_boolean()) + { + auto f_bdd = formula_to_bdd(f, d, owner); + + if (f_bdd == bddfalse) + return {}; + + return {{f_bdd, formula::eword()}}; + } + + auto rec = [&d, owner, seen](formula f){ + return expansion2(f, d, owner, exp_opts::None, seen); + }; + + + switch (f.kind()) + { + case op::ff: + case op::tt: + case op::ap: + SPOT_UNREACHABLE(); + + case op::eword: + // return {{bddfalse, formula::ff()}}; + return {}; + + case op::Concat: + { + auto exps = rec(f[0]); + + exp_t res; + for (const auto& [bdd_l, form] : exps) + { + res.push_back({bdd_l, formula::Concat({form, f.all_but(0)})}); + } + + if (f[0].accepts_eword()) + { + auto exps_rest = rec(f.all_but(0)); + for (const auto& [bdd_l, form] : exps_rest) + { + res.push_back({bdd_l, form}); + } + } + + finalize(res, opts, d, seen); + return res; + } + + case op::FStar: + { + formula E = f[0]; + + if (f.min() == 0 && f.max() == 0) + return {{bddtrue, formula::eword()}}; + + auto min = f.min() == 0 ? 0 : (f.min() - 1); + auto max = f.max() == formula::unbounded() + ? formula::unbounded() + : (f.max() - 1); + + auto E_i_j_minus = formula::FStar(E, min, max); + + auto exp = rec(E); + exp_t res; + for (const auto& [li, ei] : exp) + { + res.push_back({li, formula::Fusion({ei, E_i_j_minus})}); + + if (ei.accepts_eword() && f.min() != 0) + { + for (const auto& [ki, fi] : rec(E_i_j_minus)) + { + // FIXME: build bdd once + if ((li & ki) != bddfalse) + res.push_back({li & ki, fi}); + } + } + } + if (f.min() == 0) + res.push_back({bddtrue, formula::eword()}); + + finalize(res, opts, d, seen); + return res; + } + + case op::Star: + { + auto min = f.min() == 0 ? 0 : (f.min() - 1); + auto max = f.max() == formula::unbounded() + ? formula::unbounded() + : (f.max() - 1); + + auto exps = rec(f[0]); + + exp_t res; + for (const auto& [bdd_l, form] : exps) + { + res.push_back({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})}); + } + + finalize(res, opts, d, seen); + return res; + } + + case op::AndNLM: + { + formula rewrite = rewrite_and_nlm(f); + auto res = rec(rewrite); + finalize(res, opts, d, seen); + return res; + } + + case op::first_match: + { + auto exps = rec(f[0]); + + exp_t res; + for (const auto& [bdd_l, form] : exps) + { + res.push_back({bdd_l, form}); + } + + // determinize + bdd or_labels = bddfalse; + bdd support = bddtrue; + bool is_det = true; + for (const auto& [l, _] : res) + { + support &= bdd_support(l); + if (is_det) + is_det = !bdd_have_common_assignment(l, or_labels); + or_labels |= l; + } + + if (is_det) + { + for (auto& [_, dest] : res) + dest = formula::first_match(dest); + finalize(res, opts, d, seen); + return res; + } + + exp_t res_det; + std::vector dests; + for (bdd l: minterms_of(or_labels, support)) + { + for (const auto& [ndet_label, ndet_dest] : res) + { + if (bdd_implies(l, ndet_label)) + dests.push_back(ndet_dest); + } + formula or_dests = formula::OrRat(dests); + res_det.push_back({l, or_dests}); + dests.clear(); + } + + for (auto& [_, dest] : res_det) + dest = formula::first_match(dest); + finalize(res_det, opts, d, seen); + return res_det; + } + + case op::Fusion: + { + exp_t res; + formula E = f[0]; + formula F = f.all_but(0); + + exp_t Ei = rec(E); + // TODO: std::option + exp_t Fj = rec(F); + + for (const auto& [li, ei] : Ei) + { + if (ei.accepts_eword()) + { + for (const auto& [kj, fj] : Fj) + if ((li & kj) != bddfalse) + res.push_back({li & kj, fj}); + } + + formula ei_fusion_F = formula::Fusion({ei, F}); + if (!ei_fusion_F.is(op::ff)) + res.push_back({li, ei_fusion_F}); + } + + finalize(res, opts, d, seen); + return res; + } + + case op::AndRat: + { + exp_t res; + for (const auto& sub_f : f) + { + auto exps = rec(sub_f); + + if (exps.empty()) + { + // op::AndRat: one of the expansions was empty (the only + // edge was `false`), so the AndRat is empty as + // well + res.clear(); + break; + } + + if (res.empty()) + { + res = std::move(exps); + continue; + } + + exp_t new_res; + bool inserted = false; + for (const auto& [l_key, l_val] : exps) + { + for (const auto& [r_key, r_val] : res) + { + if ((l_key & r_key) != bddfalse) + { + new_res.push_back({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})}); + inserted = true; + } + } + } + + if (!inserted) + { + // all prefix conjuctions led to bddfalse, And is empty + res.clear(); + break; + } + + res = std::move(new_res); + } + + finalize(res, opts, d, seen); + return res; + } + + case op::OrRat: + { + exp_t res; + for (const auto& sub_f : f) + { + auto exps = rec(sub_f); + if (exps.empty()) + continue; + + if (res.empty()) + { + res = std::move(exps); + continue; + } + + for (const auto& [label, dest] : exps) + res.push_back({label, dest}); + } + + finalize(res, opts, d, seen); + return res; + } + + default: + std::cerr << "unimplemented kind " + << static_cast(f.kind()) + << std::endl; + SPOT_UNIMPLEMENTED(); + } + + return {}; + } + + twa_graph_ptr + expand_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts) + { + auto finite = expand_finite_automaton2(f, d, opts); + return from_finite(finite); + } + + struct signature_hash + { + std::size_t + operator() (const expansion_t& sig) const noexcept + { + size_t hash = 0; + + for (const auto& keyvalue : sig) + { + hash ^= (bdd_hash()(keyvalue.first) ^ std::hash()(keyvalue.second)) + + 0x9e3779b9 + (hash << 6) + (hash >> 2); + } + + return hash; + } + }; + + twa_graph_ptr + expand_finite_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts) + { + bool signature_merge = opts & exp_opts::expand_opt::SignatureMerge; + + auto aut = make_twa_graph(d); + + aut->prop_state_acc(false); + const auto acc_mark = aut->set_buchi(); + + auto formula2state = robin_hood::unordered_map(); + auto signature2state = std::unordered_map(); + auto seen = std::unordered_set(); + seen.insert(f); + + unsigned init_state = aut->new_state(); + aut->set_init_state(init_state); + formula2state.insert({ f, init_state }); + + + auto f_aps = formula_aps(f); + for (auto& ap : f_aps) + aut->register_ap(ap); + + auto formula2signature = robin_hood::unordered_map(); + auto get_signature = [&](const formula& form) -> expansion_t + { + auto it = formula2signature.find(form); + if (it != formula2signature.end()) + { + return it->second; + } + auto exp = expansion2(form, d, aut.get(), opts, &seen); + formula2signature.insert({form, exp}); + return exp; + }; + + if (signature_merge) + signature2state.insert({ get_signature(f), init_state}); + + auto todo = std::vector>(); + todo.push_back({f, init_state}); + + auto state_names = new std::vector(); + std::ostringstream ss; + ss << f; + state_names->push_back(ss.str()); + + auto find_dst = [&](formula suffix) -> unsigned + { + unsigned dst; + auto it = formula2state.find(suffix); + if (it != formula2state.end()) + { + dst = it->second; + } + else + { + if (signature_merge) + { + auto exp = get_signature(suffix); + + auto it2 = signature2state.find(exp); + if (it2 != signature2state.end()) + { + formula2state.insert({suffix, it2->second}); + return it2->second; + } + } + + dst = aut->new_state(); + todo.push_back({suffix, dst}); + seen.insert(suffix); + + formula2state.insert({suffix, dst}); + if (signature_merge) + signature2state.insert({get_signature(suffix), dst}); + + std::ostringstream ss; + ss << suffix; + state_names->push_back(ss.str()); + } + + return dst; + }; + + while (!todo.empty()) + { + auto [curr_f, curr_state] = todo[todo.size() - 1]; + todo.pop_back(); + + + auto exp = get_signature(curr_f); + + for (const auto& [letter, suffix] : exp) + { + if (suffix.is(op::ff)) + // TODO ASSERT NOT + continue; + + auto dst = find_dst(suffix); + + auto curr_acc_mark = suffix.accepts_eword() ? acc_mark : acc_cond::mark_t(); + aut->new_edge(curr_state, dst, letter, curr_acc_mark); + } + } + + aut->set_named_prop("state-names", state_names); + + if ((opts & exp_opts::MergeEdges) + && !(opts & exp_opts::UniqueSuffixPre || opts & exp_opts::UniqueSuffixPost)) + aut->merge_edges(); + + return aut; + } +} diff --git a/spot/tl/expansions2.hh b/spot/tl/expansions2.hh new file mode 100644 index 000000000..e517bb87a --- /dev/null +++ b/spot/tl/expansions2.hh @@ -0,0 +1,45 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// 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 . + +#pragma once + +#include + +#include + +#include +#include +#include +#include +#include + +namespace spot +{ + SPOT_API expansion_t + expansion2(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set* seen = nullptr); + + SPOT_API twa_graph_ptr + expand_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts); + + SPOT_API twa_graph_ptr + expand_finite_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts); + + SPOT_API formula + expansion_to_formula2(expansion_t e, bdd_dict_ptr& d); +} diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 882714ab2..d422becb0 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -230,11 +230,15 @@ namespace spot // them. }); + bool is_state_acc = this->prop_state_acc().is_true(); + unsigned out = 0; unsigned in = 1; // Skip any leading false edge. - while (in < tend && trans[in].cond == bddfalse) + while (in < tend + && trans[in].cond == bddfalse + && (!is_state_acc || trans[in].src != trans[in].dst)) ++in; if (in < tend) { @@ -243,7 +247,9 @@ namespace spot trans[out] = trans[in]; for (++in; in < tend; ++in) { - if (trans[in].cond == bddfalse) // Unusable edge + if (trans[in].cond == bddfalse + && (!is_state_acc + || trans[in].src != trans[in].dst)) // Unusable edge continue; // Merge edges with the same source, destination, and // colors. (We test the source last, because this is the diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 8e5b929d0..432f1a85d 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -99,6 +99,7 @@ twaalgos_HEADERS = \ totgba.hh \ toweak.hh \ translate.hh \ + translate_aa.hh \ word.hh \ zlktree.hh @@ -177,6 +178,7 @@ libtwaalgos_la_SOURCES = \ totgba.cc \ toweak.cc \ translate.cc \ + translate_aa.cc \ word.cc \ zlktree.cc diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index c7b2a17d5..fb95fd6f3 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -28,8 +28,8 @@ namespace spot { - outedge_combiner::outedge_combiner(const twa_graph_ptr& aut) - : aut_(aut), vars_(bddtrue) + outedge_combiner::outedge_combiner(const twa_graph_ptr& aut, unsigned sink) + : aut_(aut), vars_(bddtrue), acc_sink_(sink) { } @@ -38,7 +38,8 @@ namespace spot aut_->get_dict()->unregister_all_my_variables(this); } - bdd outedge_combiner::operator()(unsigned st) + bdd outedge_combiner::operator()(unsigned st, const std::vector& dst_filter, + bool remove_original_edges) { const auto& dict = aut_->get_dict(); bdd res = bddtrue; @@ -47,9 +48,27 @@ namespace spot bdd res2 = bddfalse; for (auto& e: aut_->out(d1)) { + // handle edge filtering + if (!dst_filter.empty()) + { + // if any edge destination is an accepting state in the SERE + // automaton, handle the edge, otherwise skip it + auto univ_dests = aut_->univ_dests(e.dst); + if (std::all_of(univ_dests.begin(), univ_dests.end(), + [&](unsigned dst) + { + return std::find(dst_filter.begin(), dst_filter.end(), dst) + == dst_filter.end(); + })) + continue; + } + bdd out = bddtrue; for (unsigned d: aut_->univ_dests(e.dst)) { + if (d == acc_sink_) + continue; + auto p = state_to_var.emplace(d, 0); if (p.second) { @@ -61,7 +80,11 @@ namespace spot out &= bdd_ithvar(p.first->second); } res2 |= e.cond & out; + + if (remove_original_edges) + e.cond = bddfalse; } + res &= res2; } return res; @@ -78,7 +101,17 @@ namespace spot { bdd cond = bdd_exist(cube, vars_); bdd dest = bdd_existcomp(cube, vars_); - while (dest != bddtrue) + + if (dest == bddtrue) + { + // if dest is bddtrue then the accepting sink is the only + // destination for this edge, in that case don't filter it out + assert(acc_sink_ != -1u); + aut_->new_edge(st, acc_sink_, cond); + continue; + } + + do { assert(bdd_low(dest) == bddfalse); auto it = var_to_state.find(bdd_var(dest)); @@ -86,6 +119,8 @@ namespace spot univ_dest.push_back(it->second); dest = bdd_high(dest); } + while (dest != bddtrue); + std::sort(univ_dest.begin(), univ_dest.end()); aut_->new_univ_edge(st, univ_dest.begin(), univ_dest.end(), cond); univ_dest.clear(); diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh index a03ddc121..8d1027e8b 100644 --- a/spot/twaalgos/alternation.hh +++ b/spot/twaalgos/alternation.hh @@ -49,10 +49,12 @@ namespace spot std::map state_to_var; std::map var_to_state; bdd vars_; + unsigned acc_sink_; public: - outedge_combiner(const twa_graph_ptr& aut); + outedge_combiner(const twa_graph_ptr& aut, unsigned sink = -1u); ~outedge_combiner(); - bdd operator()(unsigned st); + bdd operator()(unsigned st, const std::vector& dst_filter = std::vector(), + bool remove_original_edges = false); void new_dests(unsigned st, bdd out) const; }; diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 09e88acae..c5a8c9d02 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -19,9 +19,12 @@ #include "config.h" #include #include +#include #include #include #include +#include +#include #include #include #include @@ -99,15 +102,14 @@ namespace spot class ratexp_to_dfa final { typedef twa_graph::namer namer; + // Use robin_hood::pair because std::pair is not no-throw constructible + typedef robin_hood::pair labelled_aut; public: - ratexp_to_dfa(translate_dict& dict); + ratexp_to_dfa(translate_dict& dict, bool disable_scc_trimming = false); std::vector> succ(formula f); ~ratexp_to_dfa(); - protected: - // Use robin_hood::pair because std::pair is not no-throw constructible - typedef robin_hood::pair labelled_aut; labelled_aut translate(formula f); private: @@ -115,6 +117,7 @@ namespace spot typedef robin_hood::unordered_node_map f2a_t; std::vector automata_; f2a_t f2a_; + bool disable_scc_trimming_; }; // Helper dictionary. We represent formulae using BDDs to @@ -221,6 +224,7 @@ namespace spot int register_proposition(formula f) { + // TODO: call this in expansions int num = dict->register_proposition(f, this); var_set &= bdd_ithvar(num); return num; @@ -747,55 +751,7 @@ namespace spot SPOT_UNREACHABLE(); case op::AndNLM: { - unsigned s = f.size(); - vec final; - vec non_final; - - for (auto g: f) - if (g.accepts_eword()) - final.emplace_back(g); - else - non_final.emplace_back(g); - - if (non_final.empty()) - // (a* & b*);c = (a*|b*);c - return recurse_and_concat(formula::OrRat(std::move(final))); - if (!final.empty()) - { - // let F_i be final formulae - // N_i be non final formula - // (F_1 & ... & F_n & N_1 & ... & N_m) - // = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m) - // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] - formula f = formula::OrRat(std::move(final)); - formula n = formula::AndNLM(std::move(non_final)); - formula t = formula::one_star(); - formula ft = formula::Concat({f, t}); - formula nt = formula::Concat({n, t}); - formula ftn = formula::AndRat({ft, n}); - formula fnt = formula::AndRat({f, nt}); - return recurse_and_concat(formula::OrRat({ftn, fnt})); - } - // No final formula. - // Translate N_1 & N_2 & ... & N_n into - // N_1 && (N_2;[*]) && ... && (N_n;[*]) - // | (N_1;[*]) && N_2 && ... && (N_n;[*]) - // | (N_1;[*]) && (N_2;[*]) && ... && N_n - formula star = formula::one_star(); - vec disj; - for (unsigned n = 0; n < s; ++n) - { - vec conj; - for (unsigned m = 0; m < s; ++m) - { - formula g = f[m]; - if (n != m) - g = formula::Concat({g, star}); - conj.emplace_back(g); - } - disj.emplace_back(formula::AndRat(std::move(conj))); - } - return recurse_and_concat(formula::OrRat(std::move(disj))); + return recurse_and_concat(rewrite_and_nlm(f)); } case op::AndRat: { @@ -932,8 +888,22 @@ namespace spot bdd res; if (!f.is_boolean()) { - ratexp_trad_visitor v(dict, to_concat); - res = v.visit(f); + if (sere_translation_options() == 0) + { + ratexp_trad_visitor v(dict, to_concat); + res = v.visit(f); + } + else // version expansion + { + res = bddfalse; + for (auto [label, succ]: expansion(f, dict.dict, &dict, exp_opts::expand_opt::None, nullptr)) + { + if (to_concat) + succ = formula::Concat({succ, to_concat}); + int x = dict.register_next_variable(succ); + res |= label & bdd_ithvar(x); + } + } } else { @@ -948,8 +918,9 @@ namespace spot } - ratexp_to_dfa::ratexp_to_dfa(translate_dict& dict) + ratexp_to_dfa::ratexp_to_dfa(translate_dict& dict, bool disable_scc_trimming) : dict_(dict) + , disable_scc_trimming_(disable_scc_trimming) { } @@ -1002,6 +973,12 @@ namespace spot } } + if (disable_scc_trimming_) + { + automata_.emplace_back(a, namer); + return labelled_aut(a, namer); + } + // The following code trims the automaton in a crude way by // eliminating SCCs that are not coaccessible. It does not // actually remove the states, it simply marks the corresponding @@ -2226,4 +2203,99 @@ namespace spot return a; } + twa_graph_ptr + sere_to_tgba(formula f, const bdd_dict_ptr& dict, bool disable_scc_trimming) + { + // make sure we use bdd translation in this case + auto old_opt = sere_translation_options(); + sere_translation_options("bdd"); + + f = negative_normal_form(f); + + tl_simplifier* s = new tl_simplifier(dict); + twa_graph_ptr a = make_twa_graph(dict); + + translate_dict d(a, s, false, false, false); + ratexp_to_dfa sere2dfa(d, disable_scc_trimming); + + auto [dfa, namer] = sere2dfa.translate(f); + + // language was empty, build an automaton with one non accepting state + if (dfa == nullptr) + { + auto res = make_twa_graph(dict); + res->set_init_state(res->new_state()); + res->prop_universal(true); + res->prop_complete(false); + res->prop_stutter_invariant(true); + res->prop_terminal(true); + res->prop_state_acc(true); + return res; + } + + auto res = make_twa_graph(dfa, {false, false, true, false, false, false}); + + // HACK: translate_dict registers the atomic propositions in the "final" + // automaton that would be produced by a full translation, not in the + // intermediate automaton we're interested in. We can copy them from the + // resulting automaton. + res->copy_ap_of(a); + + res->prop_state_acc(true); + const auto acc_mark = res->set_buchi(); + + size_t sn = namer->state_to_name.size(); + auto names = new std::vector(sn); + for (size_t i = 0; i < sn; ++i) + { + formula g = namer->state_to_name[i]; + (*names)[i] = str_psl(g); + if (g.accepts_eword()) + { + if (res->get_graph().state_storage(i).succ == 0) + res->new_edge(i, i, bddfalse, acc_mark); + else + { + for (auto& e : res->out(i)) + e.acc = acc_mark; + } + } + } + + res->set_named_prop("state-names", names); + + // restore previous option + if (old_opt != 0) + sere_translation_options("expansion"); + + return res; + } + + int sere_translation_options(const char* version) + { + static int pref = -1; + const char *env = nullptr; + if (!version && pref < 0) + version = env = getenv("SPOT_SERE_TRANSLATE_OPT"); + if (version) + { + if (!strcasecmp(version, "bdd")) + pref = 0; + else if (!strcasecmp(version, "expansion")) + pref = 1; + else + { + const char* err = ("sere_translation_options(): argument" + " should be one of {bdd,expansion}"); + if (env) + err = "SPOT_SERE_TRANSLATE_OPT should be one of {bdd,expansion}"; + throw std::runtime_error(err); + } + } + else if (pref < 0) + { + pref = 0; + } + return pref; + } } diff --git a/spot/twaalgos/ltl2tgba_fm.hh b/spot/twaalgos/ltl2tgba_fm.hh index 717ae6b1b..7b536d6fe 100644 --- a/spot/twaalgos/ltl2tgba_fm.hh +++ b/spot/twaalgos/ltl2tgba_fm.hh @@ -89,4 +89,9 @@ namespace spot bool unambiguous = false, const output_aborter* aborter = nullptr, bool label_with_ltl = false); + + SPOT_API twa_graph_ptr + sere_to_tgba(formula f, const bdd_dict_ptr& dict, bool disable_scc_trimming = false); + + SPOT_API int sere_translation_options(const char* version = nullptr); } diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc index eb7c54dd0..092c1f50c 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -245,4 +245,51 @@ namespace spot } + twa_graph_ptr from_finite(const_twa_graph_ptr aut, const char* alive) + { + twa_graph_ptr res = + make_twa_graph(aut, + { true, false, true, false, false, false }); + + if (aut->get_named_prop>("state-names")) + res->copy_state_names_from(aut); + auto* names = res->get_named_prop>("state-names"); + + unsigned alive_sink = res->new_state(); + if (names != nullptr) + names->push_back("sink"); + auto acc = res->acc().all_sets(); + auto alive_bdd = bdd_ithvar(res->register_ap(alive)); + res->new_edge(alive_sink, alive_sink, !alive_bdd, acc); + + unsigned ns = res->num_states(); + for (unsigned s = 0; s < ns; ++s) + { + if (s == alive_sink) + continue; + + bool was_acc = res->state_is_accepting(s); + + // erase accepting marks, require alive on non-accepting transition, + // and remove self-loop edges used to mark acceptance + auto i = res->out_iteraser(s); + while (i) + { + if (i->src == i->dst && i->cond == bddfalse) + { + i.erase(); + continue; + } + + i->cond &= alive_bdd; + i->acc = {}; + ++i; + } + + if (was_acc) + res->new_edge(s, alive_sink, !alive_bdd); + } + + return res; + } } diff --git a/spot/twaalgos/remprop.hh b/spot/twaalgos/remprop.hh index ab234fed9..4121d6554 100644 --- a/spot/twaalgos/remprop.hh +++ b/spot/twaalgos/remprop.hh @@ -53,5 +53,8 @@ namespace spot SPOT_API twa_graph_ptr to_finite(const_twa_graph_ptr aut, const char* alive = "alive"); + /// \brief The opposite of the to_finite operation + SPOT_API twa_graph_ptr + from_finite(const_twa_graph_ptr aut, const char* alive = "alive"); } diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc new file mode 100644 index 000000000..095f92c5a --- /dev/null +++ b/spot/twaalgos/translate_aa.cc @@ -0,0 +1,549 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013-2018, 2020-2021 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). +// +// 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 "config.h" + +#include + +#include +#include +#include +#include +#include +#include + +#include + +namespace spot +{ + namespace + { + struct ltl_to_aa_builder + { + ltl_to_aa_builder(twa_graph_ptr aut, unsigned accepting_sink) + : aut_(aut) + , accepting_sink_(accepting_sink) + , uniq_(aut_->get_graph(), accepting_sink) + , oe_(aut_, accepting_sink) + { + } + + ~ltl_to_aa_builder() + { + aut_->get_dict()->unregister_all_my_variables(this); + } + + twa_graph_ptr aut_; + unsigned accepting_sink_; + internal::univ_dest_mapper uniq_; + outedge_combiner oe_; + + void add_self_loop(twa_graph::edge_storage_t const& e, + unsigned init_state, + acc_cond::mark_t acc) + { + if (e.dst == accepting_sink_) + { + // avoid creating a univ_dests vector if the only dest is an + // accepting sink, which can be simplified, only keeping the self + // loop + aut_->new_edge(init_state, init_state, e.cond, acc); + return; + } + + auto dests = aut_->univ_dests(e); + std::vector new_dests(dests.begin(), dests.end()); + new_dests.push_back(init_state); + + unsigned dst = uniq_.new_univ_dests(new_dests.begin(), + new_dests.end()); + aut_->new_edge(init_state, dst, e.cond, acc); + } + + unsigned copy_sere_aut_to_res(twa_graph_ptr sere_aut, + std::map& old_to_new, + std::vector* acc_states = nullptr, + bool use_accepting_sink = true) + { + unsigned ns = sere_aut->num_states(); + + // TODO: create all new states at once, keeping an initial offset (the + // number of states already present in aut_) + aut_->copy_ap_of(sere_aut); + auto register_state = [&](unsigned st) -> unsigned { + auto p = old_to_new.emplace(st, 0); + if (p.second) + { + unsigned new_st = aut_->new_state(); + p.first->second = new_st; + if (acc_states != nullptr && sere_aut->state_is_accepting(st)) + acc_states->push_back(new_st); + } + return p.first->second; + }; + + for (unsigned st = 0; st < ns; ++st) + { + unsigned new_st = register_state(st); + for (const auto& e : sere_aut->out(st)) + { + if (use_accepting_sink && sere_aut->state_is_accepting(e.dst)) + aut_->new_edge(new_st, accepting_sink_, e.cond); + else + aut_->new_edge(new_st, register_state(e.dst), e.cond); + } + } + + auto it = old_to_new.find(sere_aut->get_init_state_number()); + assert(it != old_to_new.end()); + return it->second; + } + + + unsigned recurse(formula f) + { + switch (f.kind()) + { + case op::ff: + return aut_->new_state(); + + case op::tt: + { + unsigned init_state = aut_->new_state(); + aut_->new_edge(init_state, accepting_sink_, bddtrue, {}); + return init_state; + } + + case op::ap: + case op::Not: + { + unsigned init_state = aut_->new_state(); + + bdd ap; + if (f.kind() == op::ap) + ap = bdd_ithvar(aut_->register_ap(f.ap_name())); + else + ap = bdd_nithvar(aut_->register_ap(f[0].ap_name())); + + aut_->new_edge(init_state, accepting_sink_, ap, {}); + return init_state; + } + + // FIXME: is this right for LTLf? + case op::strong_X: + case op::X: + { + unsigned sub_init_state = recurse(f[0]); + unsigned new_init_state = aut_->new_state(); + aut_->new_edge(new_init_state, sub_init_state, bddtrue, {}); + return new_init_state; + } + + case op::Or: + { + unsigned init_state = aut_->new_state(); + + for (const auto& sub_formula : f) + { + unsigned sub_init = recurse(sub_formula); + for (auto& e : aut_->out(sub_init)) + { + unsigned dst = e.dst; + if (aut_->is_univ_dest(e.dst)) + { + auto dests = aut_->univ_dests(e); + dst = uniq_.new_univ_dests(dests.begin(), dests.end()); + } + aut_->new_edge(init_state, dst, e.cond, {}); + } + } + + return init_state; + } + + case op::And: + { + unsigned init_state = aut_->new_state(); + + bdd comb = bddtrue; + for (const auto& sub_formula : f) + { + unsigned sub_init = recurse(sub_formula); + comb &= oe_(sub_init); + } + oe_.new_dests(init_state, comb); + + return init_state; + } + + case op::U: + case op::W: + { + auto acc = f.kind() == op::U + ? acc_cond::mark_t{0} + : acc_cond::mark_t{}; + + unsigned init_state = aut_->new_state(); + + unsigned lhs_init = recurse(f[0]); + unsigned rhs_init = recurse(f[1]); + + std::vector new_dests; + for (auto& e : aut_->out(lhs_init)) + add_self_loop(e, init_state, acc); + + for (auto& e : aut_->out(rhs_init)) + { + unsigned dst = e.dst; + if (aut_->is_univ_dest(e.dst)) + { + auto dests = aut_->univ_dests(e); + dst = uniq_.new_univ_dests(dests.begin(), dests.end()); + } + aut_->new_edge(init_state, dst, e.cond, {}); + } + + return init_state; + } + + case op::R: + case op::M: + { + auto acc = f.kind() == op::M + ? acc_cond::mark_t{0} + : acc_cond::mark_t{}; + + unsigned init_state = aut_->new_state(); + + unsigned lhs_init = recurse(f[0]); + unsigned rhs_init = recurse(f[1]); + + for (auto& e : aut_->out(rhs_init)) + add_self_loop(e, init_state, acc); + + bdd comb = oe_(lhs_init); + comb &= oe_(rhs_init); + oe_.new_dests(init_state, comb); + + return init_state; + } + + // F(phi) = tt U phi + case op::F: + { + auto acc = acc_cond::mark_t{0}; + + // if phi is boolean then we can reuse its initial state (otherwise + // we can't because of potential self loops) + if (f[0].is_boolean()) + { + unsigned init_state = recurse(f[0]); + aut_->new_edge(init_state, init_state, bddtrue, acc); + return init_state; + } + + unsigned init_state = aut_->new_state(); + unsigned sub_init = recurse(f[0]); + + aut_->new_edge(init_state, init_state, bddtrue, acc); + + for (auto& e : aut_->out(sub_init)) + aut_->new_edge(init_state, e.dst, e.cond, {}); + + return init_state; + } + + // G phi = ff R phi + case op::G: + { + unsigned init_state = aut_->new_state(); + + unsigned sub_init = recurse(f[0]); + + // translate like R, but only the self loop part; `ff` cancels out + // the product of edges + std::vector new_dests; + for (auto& e : aut_->out(sub_init)) + add_self_loop(e, init_state, {}); + + return init_state; + } + + case op::EConcat: + { + unsigned rhs_init = recurse(f[1]); + const auto& dict = aut_->get_dict(); + twa_graph_ptr sere_aut; + if (sere_aa_translation_options() == 0) + { + // old bdd method + sere_aut = sere_to_tgba(f[0], dict, true); + } + else if (sere_aa_translation_options() == 1) + { + // derivation + sere_aut = derive_finite_automaton_with_first(f[0], dict); + } + else + { + // linear form + sere_aut = expand_finite_automaton(f[0], dict, exp_opts::expand_opt::None); + } + + // TODO: this should be a std::vector ! + std::vector acc_states; + std::map old_to_new; + copy_sere_aut_to_res(sere_aut, old_to_new, &acc_states, false); + + std::vector acc_edges; + unsigned ns = sere_aut->num_states(); + for (unsigned st = 0; st < ns; ++st) + { + auto it = old_to_new.find(st); + assert(it != old_to_new.end()); + unsigned new_st = it->second; + + for (auto& e : aut_->out(new_st)) + { + e.acc = acc_cond::mark_t{0}; + if (std::find(acc_states.begin(), acc_states.end(), e.dst) + != acc_states.end()) + acc_edges.push_back(aut_->edge_number(e)); + } + } + + for (unsigned i : acc_edges) + { + auto& e1 = aut_->edge_storage(i); + for (const auto& e2 : aut_->out(rhs_init)) + aut_->new_edge(e1.src, e2.dst, e1.cond & e2.cond); + } + + auto it = old_to_new.find(sere_aut->get_init_state_number()); + assert(it != old_to_new.end()); + + return it->second; + } + + case op::UConcat: + { + unsigned rhs_init = recurse(f[1]); + const auto& dict = aut_->get_dict(); + twa_graph_ptr sere_aut; + if (sere_aa_translation_options() == 0) + { + // old bdd method + sere_aut = sere_to_tgba(f[0], dict, true); + } + else if (sere_aa_translation_options() == 1) + { + // derivation + sere_aut = derive_finite_automaton_with_first(f[0], dict); + } + else + { + // linear form + sere_aut = expand_finite_automaton(f[0], dict, exp_opts::expand_opt::None); + } + + // DFA recognizes the empty language, so {0} []-> rhs is always true + unsigned ns = sere_aut->num_states(); + bool has_accepting_state = false; + for (unsigned st = 0; st < ns && !has_accepting_state; ++st) + has_accepting_state = sere_aut->state_is_accepting(st); + if (!has_accepting_state) + return accepting_sink_; + + std::map old_to_new; + std::map state_to_var; + std::map var_to_state; + bdd vars = bddtrue; + bdd aps = sere_aut->ap_vars(); + std::vector univ_dest; + // TODO: this should be a std::vector ! + std::vector acc_states; + + // registers a state in various maps and returns the index of the + // anonymous bdd var representing that state + auto register_state = [&](unsigned st) -> int { + auto p = state_to_var.emplace(st, 0); + if (p.second) + { + int v = dict->register_anonymous_variables(1, this); + p.first->second = v; + + unsigned new_st = aut_->new_state(); + old_to_new.emplace(st, new_st); + var_to_state.emplace(v, new_st); + + if (sere_aut->state_is_accepting(st)) + acc_states.push_back(new_st); + + vars &= bdd_ithvar(v); + } + + return p.first->second; + }; + + aut_->copy_ap_of(sere_aut); + for (unsigned st = 0; st < ns; ++st) + { + register_state(st); + + bdd sig = bddfalse; + for (const auto& e : sere_aut->out(st)) + { + int st_bddi = register_state(e.dst); + sig |= e.cond & bdd_ithvar(st_bddi); + } + + for (bdd cond : minterms_of(bddtrue, aps)) + { + bdd dest = bdd_appex(sig, cond, bddop_and, aps); + while (dest != bddfalse) + { + assert(bdd_high(dest) == bddtrue); + auto it = var_to_state.find(bdd_var(dest)); + assert(it != var_to_state.end()); + univ_dest.push_back(it->second); + dest = bdd_low(dest); + } + + auto it = old_to_new.find(st); + assert(it != old_to_new.end()); + unsigned src = it->second; + + unsigned dst = univ_dest.empty() + ? accepting_sink_ + : (uniq_.new_univ_dests(univ_dest.begin(), + univ_dest.end())); + + aut_->new_edge(src, dst, cond, {}); + univ_dest.clear(); + } + } + + for (unsigned st = 0; st < ns; ++st) + { + auto it = old_to_new.find(st); + assert(it != old_to_new.end()); + unsigned new_st = it->second; + + bdd comb = bddtrue; + comb &= oe_(new_st, acc_states, true); + if (comb != bddtrue) + { + comb &= oe_(rhs_init); + oe_.new_dests(new_st, comb); + } + } + + auto it = old_to_new.find(sere_aut->get_init_state_number()); + assert(it != old_to_new.end()); + + aut_->merge_edges(); + return it->second; + } + + case op::Closure: + { + twa_graph_ptr sere_aut = + derive_finite_automaton_with_first(f[0], aut_->get_dict()); + std::map old_to_new; + return copy_sere_aut_to_res(sere_aut, old_to_new); + } + + case op::NegClosure: + case op::NegClosureMarked: + case op::eword: + case op::Xor: + case op::Implies: + case op::Equiv: + case op::EConcatMarked: + case op::OrRat: + case op::AndRat: + case op::AndNLM: + case op::Concat: + case op::Fusion: + case op::Star: + case op::FStar: + case op::first_match: + SPOT_UNREACHABLE(); + return -1; + } + + SPOT_UNREACHABLE(); + } + }; + } + + twa_graph_ptr + ltl_to_aa(formula f, bdd_dict_ptr& dict, bool purge_dead_states) + { + f = negative_normal_form(f); + + auto aut = make_twa_graph(dict); + aut->set_co_buchi(); + + unsigned accepting_sink = aut->new_state(); + aut->new_edge(accepting_sink, accepting_sink, bddtrue, {}); + auto builder = ltl_to_aa_builder(aut, accepting_sink); + + unsigned init_state = builder.recurse(f); + aut->set_init_state(init_state); + + if (purge_dead_states) + { + aut->purge_dead_states(); + aut->merge_edges(); + } + + return aut; + } + + int sere_aa_translation_options(const char* version) + { + static int pref = -1; + const char *env = nullptr; + if (!version && pref < 0) + version = env = getenv("SPOT_SERE_AA_TRANSLATE_OPT"); + if (version) + { + if (!strcasecmp(version, "bdd")) + pref = 0; + else if (!strcasecmp(version, "derive")) + pref = 1; + else if (!strcasecmp(version, "expansion")) + pref = 2; + else + { + const char* err = ("sere_aa_translation_options(): argument" + " should be one of {bdd,derive,expansion}"); + if (env) + err = "SPOT_SERE_AA_TRANSLATE_OPT should be one of {bdd,derive,expansion}"; + throw std::runtime_error(err); + } + } + else if (pref < 0) + { + pref = 0; + } + return pref; + } +} diff --git a/spot/twaalgos/translate_aa.hh b/spot/twaalgos/translate_aa.hh new file mode 100644 index 000000000..aedcf07d4 --- /dev/null +++ b/spot/twaalgos/translate_aa.hh @@ -0,0 +1,34 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2010-2015, 2017, 2019-2020 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de +// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. +// +// 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 . + +#pragma once + +#include +#include + +namespace spot +{ + SPOT_API twa_graph_ptr + ltl_to_aa(formula f, bdd_dict_ptr& dict, bool purge_dead_states = false); + + SPOT_API int sere_aa_translation_options(const char* version = nullptr); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 6f7abf994..9bf0cef73 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -76,6 +76,7 @@ check_PROGRAMS = \ core/intvcomp \ core/intvcmp2 \ core/kripkecat \ + core/ltl2aa \ core/ltl2dot \ core/ltl2text \ core/ltlrel \ @@ -125,6 +126,7 @@ core_cube_SOURCES = core/cube.cc core_equals_SOURCES = core/equalsf.cc core_kind_SOURCES = core/kind.cc core_length_SOURCES = core/length.cc +core_ltl2aa_SOURCES = core/ltl2aa.cc core_ltl2dot_SOURCES = core/readltl.cc core_ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY core_ltl2text_SOURCES = core/readltl.cc diff --git a/tests/core/.gitignore b/tests/core/.gitignore index d4ebfae45..fdee02715 100644 --- a/tests/core/.gitignore +++ b/tests/core/.gitignore @@ -33,6 +33,7 @@ kripkecat length .libs ikwiad +ltl2aa ltl2dot ltl2text ltlmagic diff --git a/tests/core/expand.cc b/tests/core/expand.cc new file mode 100644 index 000000000..a589d6370 --- /dev/null +++ b/tests/core/expand.cc @@ -0,0 +1,25 @@ +#include "config.h" + +#include +#include +#include +#include + +int main(int argc, char** argv) +{ + if (argc != 2) + return 1; + + spot::formula f = spot::parse_infix_sere(argv[1]).f; + auto d = spot::make_bdd_dict(); + + auto m = spot::expansion(f, d, nullptr); + + for (const auto& [bdd_l, form] : m) + std::cout << '[' << bdd_to_formula(bdd_l, d) << ']' << ": " << form << std::endl; + std::cout << "formula: " << expansion_to_formula(m, d) << std::endl; + + d->unregister_all_my_variables(nullptr); + + return 0; +} diff --git a/tests/core/ltl2aa.cc b/tests/core/ltl2aa.cc new file mode 100644 index 000000000..82b4b9c7e --- /dev/null +++ b/tests/core/ltl2aa.cc @@ -0,0 +1,22 @@ +#include "config.h" + +#include + +#include +#include +#include +#include + +int main(int argc, char * argv[]) +{ + if (argc < 3) + return 1; + + spot::formula f = spot::parse_formula(argv[1]); + spot::bdd_dict_ptr d = spot::make_bdd_dict(); + auto aut = ltl_to_aa(f, d, true); + + std::ofstream out(argv[2]); + spot::print_hoa(out, aut); + return 0; +} diff --git a/tests/core/parity2.test b/tests/core/parity2.test index 8fb35e365..b2b95f790 100755 --- a/tests/core/parity2.test +++ b/tests/core/parity2.test @@ -26,7 +26,19 @@ for x in P 'Pmin odd' 'Pmax even' p 'pmin odd' 'pmax even'; do autfilt --name=%M --high "-$x" >>res2 ltl2tgba -D "-$x" FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' >>res3 ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' | - autfilt -D --name=%M --high "-$x" >>res4 + autfilt -D --name=%M --high "-$x" >>res4 + ( + ## --colored is normally short for --colored-parity=any + ## But in case someone types something like + ## --parity='max odd' --colored + ## let's make sure we handle it like --colored-parity='max odd'. + echo "=== -$x ===" + ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' \ + "-$x" --stats='%[]g' + echo "=== -$x --colored ===" + ltl2tgba FGa 'GFa & GFb' '(p0 W XXGp0) & GFp1 & FGp2' \ + "-$x" --colored --stats='%[]g' + ) >> res5 done cat >expected<expected5 < XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2' diff --git a/tests/sanity/bin.test b/tests/sanity/bin.test index 6e9e5eafb..0ad836daa 100644 --- a/tests/sanity/bin.test +++ b/tests/sanity/bin.test @@ -52,6 +52,11 @@ do echo "bin/man/$manpage is not listed in man/Makefile.am" exit_status=2 fi + if ! grep -q "%{_mandir}/man./$manpage\*\$" $top_srcdir/spot.spec.in; + then + echo "$manpage is not listed in spot.spec.in" + exit_status=2 + fi fi case $binary in @@ -74,7 +79,7 @@ do ;; esac - # All man pages + # All tools case $manpage in *.1) if ! test -f $top_srcdir/doc/org/$binary.org; then @@ -94,8 +99,20 @@ do echo "$binary does not occur in doc/org/arch.tex" exit_status=2 fi + if ! grep -q "%{_bindir}/$binary\$" $top_srcdir/spot.spec.in; then + echo "$binary does is not listed in spot.spec.in"; + exit_status=2 + fi + esac + if test -f $top_srcdir/bin/.gitignore; then + if ! grep -q "^$binary\$" $top_srcdir/bin/.gitignore; then + echo "$binary is not listed in bin/.gitignore" + exit_status=2 + fi + fi + # Check --help text. Set a high rmargin to workaround some # bug in argp where an extra line it sometimes added if the end # of the document string fall right into the rmargin. @@ -107,6 +124,7 @@ do echo "bin/$binary --help has options after blank line;" \ "missing section header?" cat help-err + exit_status=2 fi rm -f help-$binary.tmp help-err