ks_cobuchi: forbid n=0
* spot/gen/automata.hh: State the precondition. * spot/gen/automata.cc: Catch n==0. * tests/core/genaut.test: Test it.
This commit is contained in:
parent
586f0cce7b
commit
d25cdd4c6c
3 changed files with 7 additions and 2 deletions
|
|
@ -29,6 +29,8 @@ namespace spot
|
||||||
twa_graph_ptr
|
twa_graph_ptr
|
||||||
ks_cobuchi(unsigned n)
|
ks_cobuchi(unsigned n)
|
||||||
{
|
{
|
||||||
|
if (n == 0)
|
||||||
|
throw std::runtime_error("ks_cobuchi() expects a positive argument");
|
||||||
// the alphabet has four letters:
|
// the alphabet has four letters:
|
||||||
// i, s (for sigma), p (for pi), h (for hash)
|
// i, s (for sigma), p (for pi), h (for hash)
|
||||||
// we encode this four letters alphabet thanks to two AP a and b
|
// we encode this four letters alphabet thanks to two AP a and b
|
||||||
|
|
@ -86,4 +88,3 @@ namespace spot
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -41,8 +41,9 @@ namespace spot
|
||||||
/// year={2015},
|
/// year={2015},
|
||||||
/// organization={Springer}
|
/// organization={Springer}
|
||||||
/// }
|
/// }
|
||||||
|
///
|
||||||
|
/// \pre n>0
|
||||||
SPOT_API twa_graph_ptr
|
SPOT_API twa_graph_ptr
|
||||||
ks_cobuchi(unsigned n);
|
ks_cobuchi(unsigned n);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -36,3 +36,6 @@ cat >expected <<EOF
|
||||||
7,20,48,1,Fin(0)
|
7,20,48,1,Fin(0)
|
||||||
EOF
|
EOF
|
||||||
diff out expected
|
diff out expected
|
||||||
|
|
||||||
|
genaut --ks-cobuchi=0 2>err && exit 1
|
||||||
|
grep positive err
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue