randomize: reorder state names
* src/tgbaalgos/randomize.cc: Reorder state names. * src/tgbatest/randomize.test: Add a new test.
This commit is contained in:
parent
9add895ba7
commit
93271bed6f
2 changed files with 65 additions and 1 deletions
|
|
@ -39,6 +39,16 @@ namespace spot
|
||||||
std::random_shuffle(nums.begin(), nums.end(), spot::mrand);
|
std::random_shuffle(nums.begin(), nums.end(), spot::mrand);
|
||||||
g.rename_states_(nums);
|
g.rename_states_(nums);
|
||||||
aut->set_init_state(nums[aut->get_init_state_number()]);
|
aut->set_init_state(nums[aut->get_init_state_number()]);
|
||||||
|
|
||||||
|
if (auto sn =
|
||||||
|
aut->get_named_prop<std::vector<std::string>>("state-names"))
|
||||||
|
{
|
||||||
|
unsigned sns = sn->size(); // Might be != n.
|
||||||
|
auto nn = new std::vector<std::string>(n);
|
||||||
|
for (unsigned i = 0; i < sns && i < n; ++i)
|
||||||
|
(*nn)[nums[i]] = (*sn)[i];
|
||||||
|
aut->set_named_prop("state-names", nn);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
if (randomize_transitions)
|
if (randomize_transitions)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
#!/bin/sh
|
#!/bin/sh
|
||||||
# -*- coding: utf-8 -*-
|
# -*- coding: utf-8 -*-
|
||||||
# Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
|
||||||
# l'Epita (LRDE).
|
# l'Epita (LRDE).
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# This file is part of Spot, a model checking library.
|
||||||
|
|
@ -80,3 +80,57 @@ diff 4.dot 4b.dot
|
||||||
|
|
||||||
$autfilt --randomize=foo out 2>stderr && exit 1
|
$autfilt --randomize=foo out 2>stderr && exit 1
|
||||||
grep "unknown argument for --randomize: 'f'" stderr
|
grep "unknown argument for --randomize: 'f'" stderr
|
||||||
|
|
||||||
|
|
||||||
|
# Make sure names are moved.
|
||||||
|
cat >input <<EOF
|
||||||
|
HOA: v1
|
||||||
|
States: 5
|
||||||
|
Start: 0
|
||||||
|
AP: 4 "a" "b" "c" "d"
|
||||||
|
acc-name: all
|
||||||
|
Acceptance: 0 t
|
||||||
|
properties: trans-labels explicit-labels state-acc
|
||||||
|
--BODY--
|
||||||
|
State: 0 "s0"
|
||||||
|
[0] 1
|
||||||
|
[1] 2
|
||||||
|
[2] 3
|
||||||
|
[3] 4
|
||||||
|
State: 1 "s1"
|
||||||
|
[0] 1
|
||||||
|
State: 2 "s2"
|
||||||
|
[1] 2
|
||||||
|
State: 3 "s3"
|
||||||
|
[2] 3
|
||||||
|
State: 4 "s4"
|
||||||
|
[3] 4
|
||||||
|
--END--
|
||||||
|
EOF
|
||||||
|
$autfilt --randomize --seed=1 input -H > output
|
||||||
|
cat >expected <<EOF
|
||||||
|
HOA: v1
|
||||||
|
States: 5
|
||||||
|
Start: 1
|
||||||
|
AP: 4 "a" "b" "c" "d"
|
||||||
|
acc-name: all
|
||||||
|
Acceptance: 0 t
|
||||||
|
properties: trans-labels explicit-labels state-acc
|
||||||
|
--BODY--
|
||||||
|
State: 0 "s1"
|
||||||
|
[0] 0
|
||||||
|
State: 1 "s0"
|
||||||
|
[1] 3
|
||||||
|
[0] 0
|
||||||
|
[2] 2
|
||||||
|
[3] 4
|
||||||
|
State: 2 "s3"
|
||||||
|
[2] 2
|
||||||
|
State: 3 "s2"
|
||||||
|
[1] 3
|
||||||
|
State: 4 "s4"
|
||||||
|
[3] 4
|
||||||
|
--END--
|
||||||
|
EOF
|
||||||
|
|
||||||
|
diff output expected
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue