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

cgi: Add an nondeterministic monitor option

* src/tgbaalgos/postproc.hh (run): Rename the first argument as
input_disown to help Swig.
* wrap/python/spot.i: Wrap spot::postprocessor.
* wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/protocol.txt:
Add an option for nondeterministic monitor.
* wrap/python/ajax/spot.in: Honor the new option, and rewrite the
monitor production using postprocessor.
parent c8925994
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -84,8 +84,8 @@ namespace spot
level_ = level;
}
/// Return the optimized automaton and delete \a input.
const tgba* run(const tgba* input, const ltl::formula* f);
/// Return the optimized automaton and delete \a input_disown.
const tgba* run(const tgba* input_disown, const ltl::formula* f);
private:
output_type type_;
......
......@@ -504,6 +504,10 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<INPUT type="radio" name="mf" value="d" checked>
a deterministic monitor
</label><br>
<label class="rtip" title="A nondeterministic monitor is an NFA that accepts all the prefixes of the executions that satisfy the formula.">
<INPUT type="radio" name="mf" value="n" checked>
a nondeterministic monitor
</label><br>
</div>
<div id="tabs-oa">
Translate the (simplified) formula as:<br>
......
......@@ -36,9 +36,10 @@ Type of automaton if o=a (pick one)
af=s SBA
af=i Spin neverclaim
Type of monitor if o=m (pick one -- no choice)
Type of monitor if o=m (pick one)
mf=d
mf=d deterministic
mf=n nondeterministic
Type of automaton for run if o=r (pick one)
......
......@@ -571,9 +571,15 @@ elif translator == 'l3':
# Monitor output
if output_type == 'm':
issba = False
automaton = spot.scc_filter(automaton)
automaton = spot.minimize_monitor(automaton)
issba = True
mf = form.getfirst('mf', 'd')
pp = spot.postprocessor()
pp.set_type(spot.postprocessor.Monitor)
if mf == 'd':
pp.set_pref(spot.postprocessor.Deterministic)
elif mf == 'n':
pp.set_pref(spot.postprocessor.Small)
automaton = pp.run(automaton, f)
unbufprint('<div class="automata-stats">')
dont_run_dot = print_stats(automaton)
unbufprint('</div>')
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique
// de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
......@@ -108,6 +108,7 @@ namespace std {
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
#include "tgbaalgos/simulation.hh"
#include "tgbaalgos/postproc.hh"
#include "tgbaparse/public.hh"
......@@ -211,6 +212,12 @@ using namespace spot;
%feature("new") spot::tgba_parse;
%feature("new") spot::tgba_to_ta;
%feature("new") spot::tgba_to_tgta;
%feature("new") spot::postprocessor::run;
// The argument to postprocessor::run() will be deleted.
// Apparently SWIG can only disown arguments based on their
// names...
%apply SWIGTYPE *DISOWN { SWIGTYPE * input_disown };
// Help SWIG with namespace lookups.
#define ltl spot::ltl
......@@ -297,6 +304,7 @@ using namespace spot;
%include "tgbaalgos/stats.hh"
%include "tgbaalgos/isdet.hh"
%include "tgbaalgos/simulation.hh"
%include "tgbaalgos/postproc.hh"
%include "tgbaparse/public.hh"
......
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