alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

bin: new ltlmix tool

Browse source 
Fixes #400.

* spot/tl/randomltl.cc, spot/tl/randomltl.hh: Adjust to accept
a set of formula to replace the atomic propositions.
* bin/ltlmix.cc: New file.
* bin/Makefile.am: Add it.
* bin/man/ltlmix.x: New file.
* bin/man/Makefile.am: Add it.
* doc/org/ltlmix.org: New file.
* doc/Makefile.am: Add it.
* bin/man/genltl.x, bin/man/randltl.x, bin/man/spot.x, bin/spot.cc,
doc/org/arch.tex, doc/org/concepts.org, doc/org/tools.org, NEWS: Mention
ltlmix.
* tests/core/ltlmix.test: New file.
* tests/Makefile.am: Add it.
This commit is contained in:
Alexandre Duret-Lutz 2024-08-22 17:04:48 +02:00
parent baf2778c9a
commit c8b8ac60be
18 changed files with 995 additions and 87 deletions
Download patch file Download diff file Expand all files Collapse all files

122
spot/tl/randomltl.cc
View file

@ -28,6 +28,45 @@ namespace spot
{
namespace
{
// Rename atomic propositions in f using atomic propositions drawn
// randomly from \a ap. Avoid repetition if \a ap is large
// enough. If \a lit is true, change the polarity of the atomic
// proposition randomly.
static formula
randomize_ap(formula f, const atomic_prop_set* ap, bool lit)
{
std::vector<formula> randap(ap->begin(), ap->end());
unsigned current_range = randap.size();
std::map<formula, formula> mapping;
auto relabel = [&](formula f, auto self) -> formula
{
if (f.is(op::ap))
{
// Did we already rename this AP?
if (auto it = mapping.find(f); it != mapping.end())
return it->second;
// If we exhausted all possible AP, start again
if (current_range == 0)
current_range = randap.size();
//
unsigned pos = mrand(current_range--);
formula ap = randap[pos];
std::swap(randap[current_range], randap[pos]);
if (lit && drand() < 0.5)
ap = formula::Not(ap);
return mapping[f] = ap;
}
return f.map(self, self);
};
return relabel(f, relabel);
}
static formula
ap_builder(const random_formula* rl, int n)
{
@ -38,6 +77,20 @@ namespace spot
return *i;
}
static formula
pattern_builder(const random_formula* rl, int n)
{
assert(n == 1);
(void) n;
atomic_prop_set::const_iterator i = rl->patterns()->begin();
std::advance(i, mrand(rl->patterns()->size()));
formula f = *i;
const atomic_prop_set* ap = rl->ap();
if (ap && ap->size() > 0)
f = randomize_ap(f, ap, rl->draw_literals());
return f;
}
static formula
true_builder(const random_formula*, int n)
{
@ -353,13 +406,28 @@ namespace spot
}
// Boolean formulae
random_boolean::random_boolean(const atomic_prop_set* ap)
random_boolean::random_boolean(const atomic_prop_set* ap,
const atomic_prop_set* patterns)
: random_formula(9, ap)
{
proba_[0].setup("ap", 1, ap_builder);
proba_[0].proba = ap_->size();
if (patterns)
{
proba_[0].setup("sub", 1, pattern_builder);
patterns_ = patterns;
proba_[0].proba = patterns_->size();
}
else
{
proba_[0].setup("ap", 1, ap_builder);
proba_[0].proba = ap_->size();
}
proba_[1].setup("false", 1, false_builder);
proba_[2].setup("true", 1, true_builder);
if (patterns)
{
proba_[1].proba = 0.0;
proba_[2].proba = 0.0;
}
proba_2_or_more_ = proba_2_ = proba_ + 3;
proba_[3].setup("not", 2, unop_builder<op::Not>);
proba_[4].setup("equiv", 3, binop_builder<op::Equiv>);
@ -373,10 +441,19 @@ namespace spot
// LTL formulae
void
random_ltl::setup_proba_()
random_ltl::setup_proba_(const atomic_prop_set* patterns)
{
proba_[0].setup("ap", 1, ap_builder);
proba_[0].proba = ap_->size();
if (patterns)
{
proba_[0].setup("sub", 1, pattern_builder);
patterns_ = patterns;
proba_[0].proba = patterns_->size();
}
else
{
proba_[0].setup("ap", 1, ap_builder);
proba_[0].proba = ap_->size();
}
proba_[1].setup("false", 1, false_builder);
proba_[2].setup("true", 1, true_builder);
proba_2_or_more_ = proba_2_ = proba_ + 3;
@ -395,17 +472,18 @@ namespace spot
proba_[15].setup("or", 3, multop_builder<op::Or>);
}
random_ltl::random_ltl(const atomic_prop_set* ap)
random_ltl::random_ltl(const atomic_prop_set* ap,
const atomic_prop_set* patterns)
: random_formula(16, ap)
{
setup_proba_();
setup_proba_(patterns);
update_sums();
}
random_ltl::random_ltl(int size, const atomic_prop_set* ap)
: random_formula(size, ap)
{
setup_proba_();
setup_proba_(nullptr);
// No call to update_sums(), this functions is always
// called by the random_psl constructor.
}
@ -428,7 +506,8 @@ namespace spot
const option_map& opts,
char* opt_pL,
char* opt_pS,
char* opt_pB)
char* opt_pB,
const atomic_prop_set* subs)
: opt_simpl_level_(opts.get("simplification_level", 3)),
simpl_(tl_simplifier_options{opt_simpl_level_})
{
@ -439,6 +518,7 @@ namespace spot
opt_tree_size_max_ = opts.get("tree_size_max", 15);
opt_unique_ = opts.get("unique", 1);
opt_wf_ = opts.get("wf", 0);
bool lit = opts.get("literals", 0);
const char* tok_pL = nullptr;
const char* tok_pS = nullptr;
@ -447,23 +527,25 @@ namespace spot
switch (output_)
{
case randltlgenerator::LTL:
rf_ = new random_ltl(&aprops_);
rf_ = new random_ltl(&aprops_, subs);
rf_->draw_literals(lit);
if (opt_pS)
throw std::invalid_argument("Cannot set sere priorities with "
throw std::invalid_argument("Cannot set SERE priorities with "
"LTL output");
if (opt_pB)
throw std::invalid_argument("Cannot set boolean priorities with "
throw std::invalid_argument("Cannot set Boolean priorities with "
"LTL output");
tok_pL = rf_->parse_options(opt_pL);
break;
case randltlgenerator::Bool:
rf_ = new random_boolean(&aprops_);
rf_ = new random_boolean(&aprops_, subs);
rf_->draw_literals(lit);
tok_pB = rf_->parse_options(opt_pB);
if (opt_pL)
throw std::invalid_argument("Cannot set ltl priorities with "
throw std::invalid_argument("Cannot set LTL priorities with "
"Boolean output");
if (opt_pS)
throw std::invalid_argument("Cannot set sere priorities "
throw std::invalid_argument("Cannot set SERE priorities "
"with Boolean output");
break;
case randltlgenerator::SERE:
@ -471,7 +553,7 @@ namespace spot
tok_pS = rs_->parse_options(opt_pS);
tok_pB = rs_->rb.parse_options(opt_pB);
if (opt_pL)
throw std::invalid_argument("Cannot set ltl priorities "
throw std::invalid_argument("Cannot set LTL priorities "
"with SERE output");
break;
case randltlgenerator::PSL:
@ -500,9 +582,10 @@ namespace spot
const option_map& opts,
char* opt_pL,
char* opt_pS,
char* opt_pB)
char* opt_pB,
const atomic_prop_set* subs)
: randltlgenerator(create_atomic_prop_set(aprops_n), opts,
opt_pL, opt_pS, opt_pB)
opt_pL, opt_pS, opt_pB, subs)
{
}
@ -602,4 +685,5 @@ namespace spot
{
rs_->rb.dump_priorities(os);
}
}

140
spot/tl/randomltl.hh
View file

@ -44,16 +44,33 @@ namespace spot
delete[] proba_;
}
/// Return the set of atomic proposition used to build formulae.
const atomic_prop_set*
ap() const
/// Return the set of atomic proposition used to build formulas.
const atomic_prop_set* ap() const
{
return ap_;
}
/// Return the set of patterns (sub-formulas) used to build formulas.
const atomic_prop_set* patterns() const
{
return patterns_;
}
/// Check whether relabeling APs should use literals.
bool draw_literals() const
{
return draw_literals_;
}
/// Set whether relabeling APs should use literals.
void draw_literals(bool lit)
{
draw_literals_ = lit;
}
/// \brief Generate a formula of size \a n.
///
/// It is possible to obtain formulae that are smaller than \a
/// It is possible to obtain formulas that are smaller than \a
/// n, because some simple simplifications are performed by the
/// AST. (For instance the formula <code>a | a</code> is
/// automatically reduced to <code>a</code> by spot::multop.)
@ -63,7 +80,7 @@ namespace spot
/// and atomic propositions.
std::ostream& dump_priorities(std::ostream& os) const;
/// \brief Update the priorities used to generate the formulae.
/// \brief Update the priorities used to generate the formulas.
///
/// \a options should be comma-separated list of KEY=VALUE
/// assignments, using keys from the above list.
@ -98,14 +115,16 @@ namespace spot
op_proba* proba_2_or_more_;
double total_2_and_more_;
const atomic_prop_set* ap_;
const atomic_prop_set* patterns_ = nullptr;
bool draw_literals_;
};
/// \ingroup tl_io
/// \brief Generate random LTL formulae.
/// \brief Generate random LTL formulas.
///
/// This class recursively constructs LTL formulae of a given
/// size. The formulae will use the use atomic propositions from
/// This class recursively constructs LTL formulas of a given
/// size. The formulas will use the use atomic propositions from
/// the set of propositions passed to the constructor, in addition
/// to the constant and all LTL operators supported by Spot.
///
@ -118,25 +137,26 @@ namespace spot
public:
/// Create a random LTL generator using atomic propositions from \a ap.
///
/// The default priorities are defined as follows:
/// The default priorities are defined as follows, depending on the
/// presence of \a subformulas.
///
/** \verbatim
ap n
false 1
true 1
not 1
F 1
G 1
X 1
equiv 1
implies 1
xor 1
R 1
U 1
W 1
M 1
and 1
or 1
ap n sub n
false 1 false 1
true 1 true 1
not 1 not 1
F 1 F 1
G 1 G 1
X 1 X 1
equiv 1 equiv 1
implies 1 implies 1
xor 1 xor 1
R 1 R 1
U 1 U 1
W 1 W 1
M 1 M 1
and 1 and 1
or 1 or 1
\endverbatim */
///
/// Where \c n is the number of atomic propositions in the
@ -147,18 +167,25 @@ namespace spot
/// as each constant (i.e., true and false) to be picked.
///
/// These priorities can be changed use the parse_options method.
random_ltl(const atomic_prop_set* ap);
///
/// If a set of subformulas is passed to the constructor, the generator
/// will build a Boolean formulas using patterns as atoms. Atomic
/// propositions in patterns will be rewritten randomly by drawing
/// some from \a ap. The probability of false/true to be generated
/// default to 0 in this case.
random_ltl(const atomic_prop_set* ap,
const atomic_prop_set* subformulas = nullptr);
protected:
void setup_proba_();
void setup_proba_(const atomic_prop_set* patterns);
random_ltl(int size, const atomic_prop_set* ap);
};
/// \ingroup tl_io
/// \brief Generate random Boolean formulae.
/// \brief Generate random Boolean formulas.
///
/// This class recursively constructs Boolean formulae of a given size.
/// The formulae will use the use atomic propositions from the
/// This class recursively constructs Boolean formulas of a given size.
/// The formulas will use the use atomic propositions from the
/// set of propositions passed to the constructor, in addition to the
/// constant and all Boolean operators supported by Spot.
///
@ -169,18 +196,19 @@ namespace spot
/// Create a random Boolean formula generator using atomic
/// propositions from \a ap.
///
/// The default priorities are defined as follows:
/// The default priorities are defined as follows depending on
/// the presence of \a subformulas.
///
/** \verbatim
ap n
false 1
true 1
not 1
equiv 1
implies 1
xor 1
and 1
or 1
ap n sub n
false 1 false 0
true 1 true 0
not 1 not 1
equiv 1 equiv 1
implies 1 implies 1
xor 1 xor 1
and 1 and 1
or 1 or 1
\endverbatim */
///
/// Where \c n is the number of atomic propositions in the
@ -191,14 +219,20 @@ namespace spot
/// as each constant (i.e., true and false) to be picked.
///
/// These priorities can be changed use the parse_options method.
random_boolean(const atomic_prop_set* ap);
///
/// If a set of \a subformulas is passed to the constructor, the
/// generator will build a Boolean formulas using patterns as
/// atoms. Atomic propositions in patterns will be rewritten
/// randomly by drawing some from \a ap.
random_boolean(const atomic_prop_set* ap,
const atomic_prop_set* subformulas = nullptr);
};
/// \ingroup tl_io
/// \brief Generate random SERE.
///
/// This class recursively constructs SERE of a given size.
/// The formulae will use the use atomic propositions from the
/// The formulas will use the use atomic propositions from the
/// set of propositions passed to the constructor, in addition to the
/// constant and all SERE operators supported by Spot.
///
@ -230,7 +264,7 @@ namespace spot
/// These priorities can be changed use the parse_options method.
///
/// In addition, you can set the properties of the Boolean
/// formula generator used to build Boolean subformulae using
/// formula generator used to build Boolean subformulas using
/// the parse_options method of the \c rb attribute.
random_sere(const atomic_prop_set* ap);
@ -238,10 +272,10 @@ namespace spot
};
/// \ingroup tl_io
/// \brief Generate random PSL formulae.
/// \brief Generate random PSL formulas.
///
/// This class recursively constructs PSL formulae of a given size.
/// The formulae will use the use atomic propositions from the
/// This class recursively constructs PSL formulas of a given size.
/// The formulas will use the use atomic propositions from the
/// set of propositions passed to the constructor, in addition to the
/// constant and all PSL operators supported by Spot.
class SPOT_API random_psl: public random_ltl
@ -249,7 +283,7 @@ namespace spot
public:
/// Create a random PSL generator using atomic propositions from \a ap.
///
/// PSL formulae are built by combining LTL operators, plus
/// PSL formulas are built by combining LTL operators, plus
/// three operators (EConcat, UConcat, Closure) taking a SERE
/// as parameter.
///
@ -287,11 +321,11 @@ namespace spot
/// These priorities can be changed use the parse_options method.
///
/// In addition, you can set the properties of the SERE generator
/// used to build SERE subformulae using the parse_options method
/// used to build SERE subformulas using the parse_options method
/// of the \c rs attribute.
random_psl(const atomic_prop_set* ap);
/// The SERE generator used to generate SERE subformulae.
/// The SERE generator used to generate SERE subformulas.
random_sere rs;
};
@ -307,12 +341,14 @@ namespace spot
randltlgenerator(int aprops_n, const option_map& opts,
char* opt_pL = nullptr,
char* opt_pS = nullptr,
char* opt_pB = nullptr);
char* opt_pB = nullptr,
const atomic_prop_set* subformulas = nullptr);
randltlgenerator(atomic_prop_set aprops, const option_map& opts,
char* opt_pL = nullptr,
char* opt_pS = nullptr,
char* opt_pB = nullptr);
char* opt_pB = nullptr,
const atomic_prop_set* subformulas = nullptr);
~randltlgenerator();
@ -345,4 +381,6 @@ namespace spot
random_psl* rp_ = nullptr;
random_sere* rs_ = nullptr;
};
}