diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc index 488ea0595..ceca18e15 100644 --- a/spot/gen/automata.cc +++ b/spot/gen/automata.cc @@ -74,7 +74,7 @@ namespace spot aut->new_edge(2, 1, p); for (unsigned q = 3; q <= 2*n; ++q) aut->new_edge(q, q, p); - // s does to next state (mod 2*n, 0 excluded) + // s goes to next state (mod 2*n, 0 excluded) aut->new_edge(2*n, 1, s); for (unsigned q = 1; q < 2*n; ++q) aut->new_edge(q, q+1, s); @@ -86,6 +86,11 @@ namespace spot aut->merge_edges(); aut->prop_state_acc(true); + aut->prop_universal(false); + aut->prop_complete(false); + aut->prop_inherently_weak(false); + aut->prop_stutter_invariant(false); + aut->prop_semi_deterministic(false); return aut; } @@ -107,7 +112,6 @@ namespace spot aut->new_states(3 * n + 1); aut->set_init_state(1); aut->set_buchi(); - aut->prop_state_acc(true); aut->new_acc_edge(0, n + 1, a); aut->new_edge(2 * n + 1, 0, b); @@ -119,6 +123,13 @@ namespace spot aut->new_edge(s, s + 2 * n, a); aut->new_edge(std::min(s + 2 * n + 1, 3 * n), s + 2 * n, a); } + + aut->prop_state_acc(true); + aut->prop_universal(false); + aut->prop_complete(false); + aut->prop_inherently_weak(false); + aut->prop_stutter_invariant(false); + aut->prop_semi_deterministic(false); return aut; } } diff --git a/tests/python/gen.py b/tests/python/gen.py index fc7e19067..5fac2a54e 100644 --- a/tests/python/gen.py +++ b/tests/python/gen.py @@ -27,11 +27,27 @@ from sys import exit k2 = gen.aut_pattern(gen.AUT_KS_COBUCHI, 2) assert k2.prop_state_acc() assert k2.num_states() == 5 +assert k2.prop_universal().is_false() +assert k2.prop_inherently_weak().is_false() +assert k2.prop_stutter_invariant().is_false() +assert k2.prop_semi_deterministic().is_false() +assert k2.prop_deterministic().is_false() +assert k2.prop_terminal().is_false() + # to_str is defined in the spot package, so this makes sure # the type returned by spot.gen.ks_cobuchi() is the correct one. assert 'to_str' in dir(k2) k3 = gen.aut_pattern(gen.AUT_L_NBA, 3) +assert k3.num_states() == 10 +assert k3.prop_state_acc() +assert k3.prop_universal().is_false() +assert k3.prop_inherently_weak().is_false() +assert k3.prop_stutter_invariant().is_false() +assert k3.prop_semi_deterministic().is_false() +assert k3.prop_deterministic().is_false() +assert k3.prop_terminal().is_false() + assert k2.get_dict() == k3.get_dict() try: