Commit 9a39bb3d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Add Rabin & Streett indices

parent 9cb28747
Pipeline #20694 passed with stage
in 2 minutes and 7 seconds
/* -*- coding: utf-8 -*-
** Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de
** Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de
** l'Epita.
**
** This application is free software; you can redistribute it and/or
......@@ -247,6 +247,9 @@ const styles = theme => ({
paddingBottom: 10
},
stutterdiv: {},
indexdiv: {
paddingBottom: 10
},
livenessdiv: {
paddingBottom: 10
},
......@@ -944,6 +947,41 @@ class LtlStudy extends React.Component {
</Typography>
)}
</div>
<div className={this.props.classes.indexdiv}>
<Typography variant="body2" color="primary">
Indices
</Typography>
{(res["Rabin_index"] !== null || res["Streett_index"] !== null) && (
<Table className={this.props.classes.wordtable}>
<TableBody>
<TableRow className={this.props.classes.wordtablerow}>
<TableCell
component="th"
scope="row"
className={this.props.classes.wordtablecell}
>
Rabin index:
</TableCell>
<TableCell className={this.props.classes.wordtablecellw}>
{res["Rabin_index"]}
</TableCell>
</TableRow>
<TableRow className={this.props.classes.wordtablerow}>
<TableCell
component="th"
scope="row"
className={this.props.classes.wordtablecell}
>
Streett index:
</TableCell>
<TableCell className={this.props.classes.wordtablecellw}>
{res["Streett_index"]}
</TableCell>
</TableRow>
</TableBody>
</Table>
)}
</div>
<div className={this.props.classes.satisfiabilitydiv}>
<Typography variant="body2" color="primary">
Satisfiability
......
#!/usr/bin/python3
# -*- coding: utf-8 -*-
# Copyright (C) 2018-2019 Laboratoire de Recherche et Développement de
# Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de
# l'Epita.
#
# This application is free software; you can redistribute it and/or
......@@ -331,6 +331,27 @@ def study(ltlformula, method='GET'):
else:
result['rej_word'] = None;
# Rabin and Streett indices
# This is done my calling reduce_parity() on a deterministic
# parity automaton.
# Note that f2 is relabeled, so do not attempt to reuse
# pos as-is after this block.
if not spot.is_deterministic(pos):
pos = spot.translate(f2, 'medium', 'generic', 'deterministic')
isparity, ismax, isodd = pos.acc().is_parity()
if not isparity:
pos = spot.to_parity(pos)
spot.complete_here(pos)
spot.change_parity_here(pos,
spot.parity_kind_max, spot.parity_style_any)
pos = spot.reduce_parity(pos)
isparity, ismax, isodd = pos.acc().is_parity()
assert isparity
assert ismax
ns = pos.num_sets() + 1
result['Rabin_index'] = (ns + int(isodd)) // 2
result['Streett_index'] = (ns + int(not isodd)) // 2
return jsonify(result)
# Input parameters
......
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