Commit dd87bdf8 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

wdba: adjust to work on any TωA

* src/twaalgos/minimize.cc, src/twaalgos/safety.cc,
src/twaalgos/safety.hh: Adjust.
* src/tests/wdba2.test: More tests.
parent 80808133
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
......@@ -37,3 +37,49 @@ run 0 ../ltl2tgba -Rm -kt 'Fa | XGd' > out2
cmp out expected
cmp out2 expected
cat >input <<EOF
HOA: v1
name: "XXFp1"
States: 5
Start: 4
AP: 1 "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: implicit-labels state-acc complete deterministic
--BODY--
State: 0 {0}
0 0
State: 1 {0}
3 0
State: 2
1 1
State: 3
3 0
State: 4
2 2
--END--
EOF
cat >expected <<EOF
HOA: v1
States: 4
Start: 2
AP: 1 "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: implicit-labels state-acc complete deterministic
properties: inherently-weak
--BODY--
State: 0 {0}
0 0
State: 1
3 3
State: 2
1 1
State: 3
3 0
--END--
EOF
../../bin/autfilt --small --high -C -Hi input > output
diff output expected
......@@ -493,10 +493,6 @@ namespace spot
twa_graph_ptr minimize_wdba(const const_twa_graph_ptr& a)
{
if (a->acc().uses_fin_acceptance())
throw std::runtime_error
("minimize_wdba cannot work with Fin acceptance");
hash_set* final = new hash_set;
hash_set* non_final = new hash_set;
......@@ -518,6 +514,7 @@ namespace spot
// (i.e., it is not the start of any accepting word).
scc_info sm(det_a);
sm.determine_unknown_acceptance();
unsigned scc_count = sm.scc_count();
// SCC that have been marked as useless.
std::vector<bool> useless(scc_count);
......
......@@ -25,16 +25,13 @@ namespace spot
{
bool
is_guarantee_automaton(const const_twa_graph_ptr& aut,
const scc_info* si)
scc_info* si)
{
if (aut->acc().uses_fin_acceptance())
throw std::runtime_error
("is_guarantee_automaton() does not support Fin acceptance");
// Create an scc_info if the user did not give one to us.
bool need_si = !si;
if (need_si)
si = new scc_info(aut);
si->determine_unknown_acceptance();
bool result = true;
......@@ -42,10 +39,6 @@ namespace spot
{
if (scc.is_rejecting())
continue;
// Non-rejecting SCCs should necessarily be accepting, because
// with only one self loop, there should be no ambiguity.
if (!scc.is_accepting())
return false;
// Accepting SCCs should have only one state.
auto& st = scc.states();
if (st.size() != 1)
......
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE)
// Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche
// et Développement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
//
......@@ -46,7 +46,7 @@ namespace spot
/// will be built otherwise).
SPOT_API bool
is_guarantee_automaton(const const_twa_graph_ptr& aut,
const scc_info* sm = 0);
scc_info* sm = 0);
/// \brief Whether a minimized WDBA represents a safety property.
///
......
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