alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Make sure PSL formulae are translated with the FM translation online.

Browse source 
* wrap/python/ajax/spot.in: Diagnose attempt to use LaCIM or Tau
on PSL formulae.
* wrap/python/ajax/css/ltl2tgba.css (.ltl2tgba .error): New entry.
This commit is contained in:
Alexandre Duret-Lutz 2011-12-05 18:48:42 +01:00
parent 3dfde9e85f
commit 3d183d68c8
2 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
wrap/python/ajax/css/ltl2tgba.css
View file

@ -80,6 +80,10 @@ div.ltl2tgba {
font-size: 1.1em; font-size: 1.1em;
} }
.ltl2tgba .error {
color: red;
}
.ltl2tgba .parse-error { .ltl2tgba .parse-error {
font-family: monospace; font-family: monospace;
white-space: pre; white-space: pre;

6
wrap/python/ajax/spot.in
View file

@ -369,6 +369,12 @@ if output_type == 'f':
# Formula translation. # Formula translation.
translator = form.getfirst('t', 'fm') translator = form.getfirst('t', 'fm')
if f.is_psl_formula() and not f.is_ltl_formula() and translator != 'fm':
print ('''<div class="error">The PSL formula
<span class="formula spot-format">%s</span>
cannot be translated using this algorithm. Please use Couveur/FM.''' % f);
finish()
dict = spot.bdd_dict() dict = spot.bdd_dict()
if translator == 'fm': if translator == 'fm':