spot: Add 'langmap' option with dichotomy (it helps to choose min val)

* python/spot/__init__.py: Handle 'dicho' option in 'sat_minimize'.
* spot/priv/satcommon.cc: Implement get_number_of_distinct_vals.
* spot/priv/satcommon.hh: Declare get_number_of_distinct_vals.
* spot/twaalgos/dtbasat.cc: Use get_number_of_distinct_vals.
* spot/twaalgos/dtbasat.hh: Change dichotomy function's prototype.
* spot/twaalgos/dtwasat.cc: Use get_number_of_distinct_vals.
* spot/twaalgos/dtwasat.hh: Change dichotomy function's prototype.
Handle options.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Add dicho_langmap_ var for options.
* tests/core/satmin2.test: Add tests for dichotomy.
* tests/core/satmin.test: Add tests for dichotomy.
* tests/python/satmin.py: Replace 'dichotomy' with 'dicho' option.
parent 7046a496
......@@ -858,7 +858,7 @@ for fun in ['remove_x', 'relabel', 'relabel_bse',
# Better interface to the corresponding C++ function.
def sat_minimize(aut, acc=None, colored=False,
state_based=False, states=0,
max_states=0, dichotomy=False,
max_states=0, dicho=False,
param=0, incr=False, assume=False):
args=''
if acc is not None:
......@@ -875,8 +875,8 @@ def sat_minimize(aut, acc=None, colored=False,
if type(max_states) is not int or max_states < 0:
raise ValueError("argument 'states' should be a positive integer")
args += ',max-states=' + str(max_states)
if dichotomy:
args += ',dichotomy'
if dicho:
args += ',dicho';
if param:
args += ',param=' + str(param)
if incr:
......
......@@ -19,6 +19,7 @@
#include <fstream>
#include <set>
#include <assert.h>
#include <spot/misc/escape.hh>
#include <spot/priv/satcommon.hh>
......@@ -185,4 +186,13 @@ namespace spot
out << "\"\n";
}
}
int
get_number_of_distinct_vals(std::vector<unsigned> v)
{
std::set<unsigned> distinct;
for (auto it = v.begin(); it != v.end(); ++it)
distinct.insert(*it);
return distinct.size();
}
}
......@@ -21,6 +21,7 @@
#include <tuple>
#include <sstream>
#include <vector>
#include <spot/misc/bddlt.hh>
#include <spot/misc/satsolver.hh>
#include <spot/misc/timer.hh>
......@@ -235,4 +236,8 @@ public:
void
print_log(timer_map& t, int target_state_number, twa_graph_ptr& res,
satsolver& solver);
/// \brief Returns the number of distinct values containted in a vector.
int
get_number_of_distinct_vals(std::vector<unsigned> v);
}
......@@ -25,6 +25,7 @@
#include <spot/misc/timer.hh>
#include <spot/priv/satcommon.hh>
#include <spot/twaalgos/dtbasat.hh>
#include <spot/twaalgos/langmap.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/stats.hh>
......@@ -1005,11 +1006,19 @@ namespace spot
twa_graph_ptr
dtba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
bool state_based, int max_states)
bool state_based, bool langmap, int max_states)
{
trace << "Dichomoty\n";
if (max_states < 0)
max_states = stats_reachable(a).states - 1;
int min_states = 1;
if (langmap)
{
trace << "Langmap\n";
std::vector<unsigned> v = language_map(a);
min_states = get_number_of_distinct_vals(v);
}
trace << "min_states=" << min_states << '\n';
twa_graph_ptr prev = nullptr;
while (min_states <= max_states)
......
......@@ -64,6 +64,7 @@ namespace spot
SPOT_API twa_graph_ptr
dtba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
bool state_based = false,
bool langmap = false,
int max_states = -1);
/// \brief Attempt to minimize a det. TBA with a SAT solver.
......
......@@ -30,6 +30,7 @@
#include <spot/twaalgos/dtbasat.hh>
#include <spot/twaalgos/dtwasat.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/langmap.hh>
#include <spot/twaalgos/postproc.hh>
#include <spot/twaalgos/sbacc.hh>
#include <spot/twaalgos/sccfilter.hh>
......@@ -1338,12 +1339,20 @@ namespace spot
dtwa_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based, int max_states,
bool colored)
bool state_based, bool langmap,
int max_states, bool colored)
{
trace << "Dichotomy\n";
if (max_states < 1)
max_states = stats_reachable(a).states - 1;
int min_states = 1;
if (langmap)
{
trace << "Langmap\n";
std::vector<unsigned> v = language_map(a);
min_states = get_number_of_distinct_vals(v);
}
trace << "min_states=" << min_states << '\n';
twa_graph_ptr prev = nullptr;
while (min_states <= max_states)
......@@ -1382,10 +1391,11 @@ namespace spot
throw std::runtime_error
("SAT-based minimization only works with deterministic automata");
bool dicho = om.get("dichotomy", 0);
bool incr = om.get("incr", 0);
bool assume = om.get("assume", 0);
int param = om.get("param", 0);
bool dicho = om.get("dicho", 0);
bool dicho_langmap = om.get("langmap", 0);
int states = om.get("states", -1);
int max_states = om.get("max-states", -1);
auto accstr = om.get_str("acc");
......@@ -1492,9 +1502,12 @@ namespace spot
a = dtwa_sat_minimize_assume(a, nacc, target_acc, state_based,
max_states, colored, param);
else if (dicho)
a = dtwa_sat_minimize_dichotomy
(a, nacc, target_acc, state_based, dicho_langmap, max_states,
colored);
else
a = (dicho ? dtwa_sat_minimize_dichotomy
: dtwa_sat_minimize)
a = dtwa_sat_minimize
(a, nacc, target_acc, state_based, max_states, colored);
}
else
......@@ -1505,10 +1518,12 @@ namespace spot
else if (assume)
a = dtba_sat_minimize_assume(a, state_based, max_states, assume);
else if (dicho)
a = dtba_sat_minimize_dichotomy
(a, state_based, dicho_langmap, max_states);
else
a = (dicho ? dtba_sat_minimize_dichotomy
: dtba_sat_minimize)
(a, state_based, max_states);
a = dtba_sat_minimize(a, state_based, max_states);
}
if (!a && !user_supplied_acc)
......
......@@ -80,6 +80,7 @@ namespace spot
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based = false,
bool langmap = false,
int max_states = -1,
bool colored = false);
......
......@@ -71,6 +71,7 @@ namespace spot
tba_determinisation_ = opt->get("tba-det", 0);
sat_minimize_ = opt->get("sat-minimize", 0);
param_ = opt->get("param", 0);
dicho_langmap_ = opt->get("langmap", 0);
sat_acc_ = opt->get("sat-acc", 0);
sat_states_ = opt->get("sat-states", 0);
state_based_ = opt->get("state-based", 0);
......@@ -429,7 +430,8 @@ namespace spot
else if (sat_minimize_ == 1 || sat_minimize_ == -1)
res = dtba_sat_minimize(res, state_based_);
else if (sat_minimize_ == 2)
res = dtba_sat_minimize_dichotomy(res, state_based_);
res = dtba_sat_minimize_dichotomy
(res, state_based_, dicho_langmap_);
else if (sat_minimize_ == 3)
res = dtba_sat_minimize_incr(res, state_based_, -1, param_);
else // if (sat_minimize == 4)
......@@ -451,7 +453,7 @@ namespace spot
res = dtwa_sat_minimize_dichotomy
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
state_based_);
state_based_, dicho_langmap_);
else if (sat_minimize_ == 3)
res = dtwa_sat_minimize_incr
(res, target_acc,
......
......@@ -190,6 +190,7 @@ namespace spot
bool tba_determinisation_ = false;
int sat_minimize_ = 0;
int param_ = 0;
bool dicho_langmap_ = false;
int sat_acc_ = 0;
int sat_states_ = 0;
bool state_based_ = false;
......
This diff is collapsed.
......@@ -61,16 +61,22 @@ diff output expected
ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=3,param=0' "GF(a <-> XXb)" -H >out
ltl2tgba -BD -x sat-minimize=2 "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=3,param=1' "GF(a <-> XXb)" -H >out
ltl2tgba -BD -x 'sat-minimize=2,langmap' "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=3,param=2' "GF(a <-> XXb)" -H >out
ltl2tgba -BD -x 'sat-minimize=4,param=0' "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=3,param=50' "GF(a <-> XXb)" -H >out
ltl2tgba -BD -x 'sat-minimize=4,param=1' "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=4,param=2' "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=4,param=50' "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out
ltl2tgba -BD -x 'sat-minimize=3,param=-1' "GF(a <-> XXb)" -H >out
......@@ -128,6 +134,11 @@ EOF
# automata.
$autfilt --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa --stats=%s >output
test `cat output` = 1
$autfilt --sat-minimize='dicho,acc="Fin(0)|Inf(1)"' test.hoa --stats=%s >output
test `cat output` = 1
$autfilt --sat-minimize='dicho,langmap,acc="Fin(0)|Inf(1)"' test.hoa \
--stats=%s >output
test `cat output` = 1
$autfilt --sat-minimize='acc="Fin(0)|Inf(1)",assume,param=0' test.hoa \
--stats=%s >output
test `cat output` = 1
......@@ -161,6 +172,12 @@ test `cat output` = 1
$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa \
--stats=%s > output
test `cat output` = 3
$autfilt -S --sat-minimize='dicho,acc="Fin(0)|Inf(1)"' test.hoa \
--stats=%s > output
test `cat output` = 3
$autfilt -S --sat-minimize='dicho,langmap,acc="Fin(0)|Inf(1)"' test.hoa \
--stats=%s > output
test `cat output` = 3
$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)",assume,param=0' test.hoa \
--stats=%s > output
test `cat output` = 3
......@@ -199,6 +216,22 @@ grep 'States: 3' output
grep 'acc-name: parity max even 3' output
grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output
test 3 = `grep -c 'State: [012] {[012]}' output`
$autfilt -S --sat-minimize='acc="parity max even 3",colored,dicho' -H \
test.hoa > output
cat output
grep 'properties:.*colored' output
grep 'States: 3' output
grep 'acc-name: parity max even 3' output
grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output
test 3 = `grep -c 'State: [012] {[012]}' output`
$autfilt -S --sat-minimize='acc="parity max even 3",colored,dicho,langmap' -H \
test.hoa > output
cat output
grep 'properties:.*colored' output
grep 'States: 3' output
grep 'acc-name: parity max even 3' output
grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output
test 3 = `grep -c 'State: [012] {[012]}' output`
$autfilt -S --sat-minimize='acc="parity max even 3",colored,assume,param=0' \
-H test.hoa > output
cat output
......@@ -306,6 +339,10 @@ State: 0
EOF
$autfilt -H --sat-minimize special.hoa > output
diff output expected
$autfilt -H --sat-minimize='dicho' special.hoa > output
diff output expected
$autfilt -H --sat-minimize='dicho,langmap' special.hoa > output
diff output expected
$autfilt -H --sat-minimize='assume,param=0' special.hoa > output
diff output expected
$autfilt -H --sat-minimize='assume,param=1' special.hoa > output
......@@ -343,6 +380,12 @@ EOF
$autfilt --sat-minimize='acc="Streett 1",max-states=2' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Streett 1",max-states=2,dicho' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Streett 1",max-states=2,dicho,langmap' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Streett 1",max-states=2,assume,param=0' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
......@@ -375,6 +418,12 @@ test "`cat out`" = 1
$autfilt --sat-minimize='acc="Rabin 1",max-states=4' foo.hoa \
--stats=%s >out && exit 1
test -z "`cat out`"
$autfilt --sat-minimize='acc="Rabin 1",max-states=4,dicho' foo.hoa \
--stats=%s >out && exit 1
test -z "`cat out`"
$autfilt --sat-minimize='acc="Rabin 1",max-states=4,dicho,langmap' foo.hoa \
--stats=%s >out && exit 1
test -z "`cat out`"
$autfilt --sat-minimize='acc="Rabin 1",max-states=4,assume,param=0' foo.hoa \
--stats=%s >out && exit 1
test -z "`cat out`"
......@@ -407,6 +456,12 @@ test -z "`cat out`"
$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1,dicho' foo.hoa \
--stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1,dicho,langmap' \
foo.hoa --stats=%s >out
test "`cat out`" = 1
$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1,assume,param=0' \
foo.hoa --stats=%s >out
test "`cat out`" = 1
......
......@@ -29,6 +29,9 @@ assert aut.is_deterministic()
min1 = spot.sat_minimize(aut, acc='Rabin 1')
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', dicho=True)
assert min1.num_sets() == 2
assert min1.num_states() == 2
min1 = spot.sat_minimize(aut, acc='Rabin 1', assume=True)
assert min1.num_sets() == 2
assert min1.num_states() == 2
......@@ -64,6 +67,9 @@ assert min1.num_sets() == 2
assert min1.num_states() == 2
min2 = spot.sat_minimize(aut, acc='Streett 2', dicho=True)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min2 = spot.sat_minimize(aut, acc='Streett 2', assume=True)
assert min2.num_sets() == 4
assert min2.num_states() == 1
......@@ -100,7 +106,7 @@ assert min2.num_states() == 1
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, dichotomy=True)
state_based=True, max_states=5, dicho=True)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min3 = spot.sat_minimize(aut, acc='Rabin 2',
......@@ -150,7 +156,7 @@ assert min3.num_states() == 3
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, dichotomy=True)
colored=True, dicho=True)
assert min4.num_sets() == 3
assert min4.num_states() == 2
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment