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

postproc: disable WDBA-minimization on request

Browse source 
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh:
Implement the wdba-minimize option.
* src/bin/spot-x.cc (wdba-minimize): Document.
* src/bin/man/spot-x.x: Update references.
This commit is contained in:
Alexandre Duret-Lutz 2013-08-21 17:53:01 +02:00
parent bfbe5b448b
commit b09ef5bea9
4 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/bin/man/spot-x.x
View file

@ -18,7 +18,7 @@ Describes the WDBA-minimization algorithm implemented in Spot.
2. 2.
Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský,
Jan Strejček: Compositional Approach to Suspension and Other Jan Strejček: Compositional Approach to Suspension and Other
Improvements to LTL Translation. Proceedings of SPIN'13. LNCS XXXX. Improvements to LTL Translation. Proceedings of SPIN'13. LNCS 7976.
Describes the compositional suspension, the simulation-based Describes the compositional suspension, the simulation-based
reductions, and the SCC-based simplifications. reductions, and the SCC-based simplifications.
@ -26,3 +26,4 @@ reductions, and the SCC-based simplifications.
[SEE ALSO] [SEE ALSO]
.BR ltl2tgba (1) .BR ltl2tgba (1)
.BR ltl2tgta (1) .BR ltl2tgta (1)
.BR dstar2tgba (1)

2
src/bin/spot-x.cc
View file

@ -90,6 +90,8 @@ on the Büchi automaton (i.e., after degeneralization has been performed). \
Set to 1 to use only direct simulation. Set to 2 to use only reverse \ Set to 1 to use only direct simulation. Set to 2 to use only reverse \
simulation. Set to 3 to iterate both direct and reverse simulations. \ simulation. Set to 3 to iterate both direct and reverse simulations. \
The default is 3 in --high mode, and 0 otherwise.") }, The default is 3 in --high mode, and 0 otherwise.") },
{ DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization. \
Enabled by default.") },
{ 0, 0, 0, 0, 0, 0 } { 0, 0, 0, 0, 0, 0 }
}; };

3
src/tgbaalgos/postproc.cc
View file

@ -59,6 +59,7 @@ namespace spot
if (dtgba_sat_minimize_ == -1 && dtgba_sat_minimize_acc_ >= 0) if (dtgba_sat_minimize_ == -1 && dtgba_sat_minimize_acc_ >= 0)
dtgba_sat_minimize_ = 0; dtgba_sat_minimize_ = 0;
state_based_ = opt->get("state-based", 0); state_based_ = opt->get("state-based", 0);
wdba_minimize_ = opt->get("wdba-minimize", 1);
} }
} }
@ -200,7 +201,7 @@ namespace spot
// (Small,Low) is the only configuration where we do not run // (Small,Low) is the only configuration where we do not run
// WDBA-minimization. // WDBA-minimization.
if (pref_ != Small || level_ != Low) if ((pref_ != Small || level_ != Low) && wdba_minimize_)
{ {
bool reject_bigger = (pref_ == Small) && (level_ == Medium); bool reject_bigger = (pref_ == Small) && (level_ == Medium);
dba = minimize_obligation(a, f, 0, reject_bigger); dba = minimize_obligation(a, f, 0, reject_bigger);

1
src/tgbaalgos/postproc.hh
View file

@ -110,6 +110,7 @@ namespace spot
int dtgba_sat_minimize_; int dtgba_sat_minimize_;
int dtgba_sat_minimize_acc_; int dtgba_sat_minimize_acc_;
bool state_based_; bool state_based_;
bool wdba_minimize_;
}; };
/// @} /// @}
} }