Commit d46da963 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

python: better interface for sat_minimize()

* NEWS: Mention it.
* wrap/python/spot.py: Rewrite the sat_minimize() function.
* wrap/python/tests/satmin.py: New file.
* wrap/python/tests/Makefile.am (TESTS): Add it.
parent c1bfc5d5
......@@ -66,6 +66,7 @@ New in spot 1.99.5a (not yet released)
Python:
* Add bindings for is_unambiguous().
* Better interface for sat_minimize().
Bug fixes:
* automaton parser was ignoring the "unambiguous" property.
......
......@@ -846,3 +846,29 @@ for fun in dir(formula):
for fun in ['remove_x', 'relabel', 'relabel_bse',
'simplify', 'unabbreviate']:
_addmap(fun)
# Better interface to the corresponding C++ function.
def sat_minimize(aut, acc=None, colored=False,
state_based=False, states=0,
max_states=0, dichotomy=False):
args=''
if acc is not None:
if type(acc) is not str:
raise ValueError("argument 'acc' should be a string")
args += ',acc="' + acc + '"'
if colored:
args += ',colored'
if states:
if type(states) is not int or states < 0:
raise ValueError("argument 'states' should be a positive integer")
args += ',states=' + str(states)
if max_states:
if type(max_states) is not int or max_states < 0:
raise ValueError("argument 'states' should be a positive integer")
args += ',max-states=' + str(max_states)
if dichotomy:
args += ',dichotomy';
from spot_impl import sat_minimize as sm
return sm(aut, args, state_based)
......@@ -53,6 +53,7 @@ TESTS = \
randltl.ipynb \
relabel.py \
remfin.py \
satmin.py \
setxor.py \
testingaut.ipynb
......
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement
# de l'Epita
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
import shutil
import sys
import spot
# Ignore the test if glucose is not installed.
if shutil.which("glucose") == None:
sys.exit(77)
aut = spot.translate('GFa & GFb', 'BA')
assert aut.num_sets() == 1
assert aut.num_states() == 3
assert aut.is_deterministic()
min1 = spot.sat_minimize(aut, acc='Rabin 1')
assert min1.num_sets() == 2
assert min1.num_states() == 2
min2 = spot.sat_minimize(aut, acc='Streett 2', dichotomy=True)
assert min2.num_sets() == 4
assert min2.num_states() == 1
min3 = spot.sat_minimize(aut, acc='Rabin 2',
state_based=True, max_states=5, dichotomy=True)
assert min3.num_sets() == 4
assert min3.num_states() == 3
min4 = spot.sat_minimize(aut, acc='parity max odd 3',
colored=True, dichotomy=True)
assert min4.num_sets() == 3
assert min4.num_states() == 2
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