diff --git a/ChangeLog b/ChangeLog index 4faf8b2d3..e1a071deb 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,30 @@ +2012-02-25 Alexandre Duret-Lutz + + Make all python code compatible with Python 2.x and Python 3.x. + + * wrap/python/buddy.i (__le__, __lt__, __eq__, __ne__, __ge__ + __gt__): New operators for bdd. + * wrap/python/spot.i (__le__, __lt__, __eq__, __ne__, __ge__ + __gt__, __hash__): New operators for formula. + (nl_cout, nl_cerr): New functions. + * wrap/python/tests/bddnqueen.py, + wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py, + wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py, + wrap/python/tests/minato.py, wrap/python/tests/modgray.py: Adjust + to the new print syntax by using sys.output.write() or nl_cout() + instead. + * wrap/python/tests/optionmap.py: Remove all print calls. + * wrap/python/ajax/spot.in: Massive adjustments in order to work + with both Python 2 and 3. In python 3, reopening stdout as + unbuffered requires it to be open as binary, which in turns + requires any string output to be encoded manually. BaseHTTPServer + and CGIHTTPServer have been merged into http.server, so we have + to try two different import syntaxes. execfile no longer exists, + so it has to be emulated. + This also fixes two bugs where the script would segfault on + empty input, or when calling Tau03 on automata with less then + one acceptance conditions. + 2012-02-24 Alexandre Duret-Lutz Fix computation of PYTHONINC for Python 3. diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 670e8e8d2..18425b35e 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -1,6 +1,6 @@ #!@PYTHON@ -# -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -21,13 +21,16 @@ # 02111-1307, USA. import os +import sys -script = os.environ.has_key('SCRIPT_NAME') +script = ('SCRIPT_NAME' in os.environ) if script: - print "Cache-Control: max-age=3600" # One hour. - print "Content-Type: text/html" - print + # 3600s = 1h + sys.stdout.write("""Cache-Control: max-age=3600 +Content-Type: text/html + +""") # Directory for temporary files (images and other auxiliary files). imgdir = 'spotimg' @@ -37,12 +40,17 @@ qs = os.getenv('QUERY_STRING') if qs: import hashlib # We (optimistically) assume no collision from sha1(qs) - cachedir = imgdir + '/' + hashlib.sha1(qs).hexdigest() + cachedir = imgdir + '/' + hashlib.sha1(qs.encode('utf-8')).hexdigest() cachename = cachedir + '/html' try: # Is this a request we have already processed? - cache = open(cachename, "r", 0) - print cache.read() + cache = open(cachename, "rb", 0) + if hasattr(sys.stdout, 'buffer'): + # Python 3+ + sys.stdout.buffer.write(cache.read()) + else: + # Python 2.x + sys.stdout.write(cache.read()) # Touch the directory containing the files we used, so # it that it survives the browser's cache. os.utime(cachedir, None) @@ -52,7 +60,7 @@ if qs: # Let's run the rest of the script to create it. pass elif script: - print "QUERY_STRING unset!" + sys.stdout.write("QUERY_STRING unset!\n") exit(0) # Location of the dot command @@ -64,26 +72,33 @@ svg_output = False # FIXME: SVG output seems to be working well with # to get the correct size and transparent # background in Chrome. -from CGIHTTPServer import CGIHTTPRequestHandler -class MyHandler(CGIHTTPRequestHandler): - def is_cgi(self): - if self.path.startswith('/cgi-bin/spot.py'): - self.cgi_info = '', self.path[9:] - return True - return False - if not script: # If this is not run as a cgi script, let's start an HTTP server. - from BaseHTTPServer import HTTPServer + try: + # Python 3+ + from http.server import CGIHTTPRequestHandler, HTTPServer + except ImportError: + # Python 2.x + from CGIHTTPServer import CGIHTTPRequestHandler + from BaseHTTPServer import HTTPServer + + class MyHandler(CGIHTTPRequestHandler): + def is_cgi(self): + if self.path.startswith('/cgi-bin/spot.py'): + self.cgi_info = '', self.path[9:] + return True + return False + server_address=('',8000) if not os.access(imgdir, os.F_OK): - os.mkdir(imgdir, 0755) - print "Directory spotimg/ created." + # 493 = 0755 but we would have to write 0755 or 0o755 + # depending on the python version... + os.mkdir(imgdir, 493) + sys.stdout.write("Directory spotimg/ created.\n") httpd = HTTPServer(server_address, MyHandler) - print "Point your browser to http://localhost:8000/ltl2tgba.html" + sys.stdout.write("Point your browser to http://localhost:8000/ltl2tgba.html\n") httpd.serve_forever() -import sys import cgi import cgitb; cgitb.enable() import signal @@ -97,25 +112,34 @@ cachename = tmpdir + '/html' sys.stdout.flush() # Reopen stdout without buffering -sys.stdout = os.fdopen(sys.stdout.fileno(), "w", 0) +sys.stdout = os.fdopen(sys.stdout.fileno(), "wb", 0) # Redirect stderr to stdout at a low level (so that # even errors from subprocesses get printed). os.dup2(sys.stdout.fileno(), sys.stderr.fileno()) # Create the temporary cache directory -os.mkdir(tmpdir, 0755) +os.mkdir(tmpdir, 493) # See comment above about 0o755 or 0755. # Redirect stdout to the cache file, at a low level # for similar reason. -fd = os.open(cachename, os.O_CREAT | os.O_WRONLY, 0644) +fd = os.open(cachename, os.O_CREAT | os.O_WRONLY, 420) # 420 = 0644 os.dup2(fd, sys.stdout.fileno()) +# We had to reopen stdout in binary mode to enable unbuffered output, +# (disallowed on text I/O by Python 3.x) so starting now, we are not +# allowed to send strings to sys.stdout. Always use the following +# method instead. +def unbufprint(s): + sys.stdout.write(s.encode("utf-8")) + + def finish(kill = False): # Output the result and exit. os.dup2(sys.stderr.fileno(), sys.stdout.fileno()) - cache = open(cachename, "r", 0) - print cache.read() + + cache = open(cachename, "rb", 0) + sys.stdout.write(cache.read()) # Rename tmpdir to its permanent name for caching purpose. # os.rename will fail if cachedir already exist. Since we tested @@ -131,6 +155,7 @@ def finish(kill = False): pass if kill: + # Kill all children os.kill(0, signal.SIGTERM) # Should we prune the cache? stamp = imgdir + '/cache.stamp' @@ -140,6 +165,8 @@ def finish(kill = False): if now - os.path.getmtime(stamp) < 3600: exit(0) except OSError: + # It's OK if the file did not exist. + # We will create it. pass # Erase all directories that are older than 2 hours, and all # files that have only one hardlinks. Files that have more than @@ -148,14 +175,14 @@ def finish(kill = False): os.system('find ' + imgdir + ' -mindepth 1 -maxdepth 1 -mmin +120 ' + '\( -type d -o -links 1 \) -exec rm -rf {} +') # Create or update the stamp so we know when to run the next prune. - open(stamp, "w", 0) + open(stamp, "wb", 0) exit(0) # Assume Spot is installed sys.path.insert(0, '@pythondir@') -if (os.environ.has_key('SERVER_SOFTWARE') and - os.environ['SERVER_SOFTWARE'].startswith(MyHandler.server_version)): +if ('SERVER_SOFTWARE' in os.environ and + os.environ['SERVER_SOFTWARE'].startswith('SimpleHTTP')): # We might be running from the build tree (but it's not sure). # Add the build and source directories first in the search path. # If we are not in the right place, python will find the installed @@ -171,7 +198,9 @@ if (os.environ.has_key('SERVER_SOFTWARE') and os.environ['DYLD_LIBRARY_PATH'] = m try: - execfile('ltl2tgba.opt') + # execfile('ltl2tgba.opt') no longuer work with Python 3. + exec(compile(open("ltl2tgba.opt").read(), "ltl2tgba.opt", 'exec'), + global_vars, local_vars) except IOError: pass @@ -179,18 +208,18 @@ import spot import buddy def alarm_handler(signum, frame): - print """

The script was aborted because + unbufprint("""

The script was aborted because it has been running for too long. Please try a shorter formula, or different options (not drawing automata usually helps). If you want to benchmark big formulae it is -better to install Spot on your own computer.

""" +better to install Spot on your own computer.

\n""") finish(kill = True) def reset_alarm(): signal.alarm(30) def render_dot(basename): - print '
' + unbufprint('
') if svg_output: ext = 'svg' else: @@ -207,32 +236,32 @@ def render_dot(basename): os.link(outname, tmpdir + "/" + ext) b = cgi.escape(basename) if svg_output: - print ('' - + 'Your browser does not support SVG.') + unbufprint('Your browser does not support SVG.') else: - print ('
(dot source)') - print '
' + unbufprint('
(dot source)') + unbufprint('
\n') def render_dot_maybe(dotsrc, dont_run_dot): # The dot output is named after the SHA1 of the dot source. # This way we can cache two different requests that generate # the same automaton (e.g., when changing a simplification # option that has no influence). - autprefix = imgdir + '/' + hashlib.sha1(dotsrc).hexdigest() + autprefix = (imgdir + '/' + hashlib.sha1(dotsrc).hexdigest()) dotname = autprefix + '.txt' if not os.access(dotname, os.F_OK): - dotout = open(dotname, "w", 0) + dotout = open(dotname, "wb", 0) dotout.write(dotsrc) dotout.close() - # Create an unused hardlink that points to the output picture + # Create a unused hardlink that points to the output picture # just to remember how many cache entries are sharing it. os.link(dotname, tmpdir + "/txt") if dont_run_dot: - print ('

' + dont_run_dot + ''' to be rendered on-line. However -you may download the source in dot format and render it yourself.') + unbufprint('

' + dont_run_dot + ''' to be rendered on-line. +However you may download the source in dot format and render it yourself.

\n') else: render_dot(autprefix) @@ -242,7 +271,7 @@ def render_automaton(automaton, dont_run_dot, issba, deco = False): spot.dotty_reachable(dotsrc, automaton, issba) else: spot.dotty_reachable(dotsrc, automaton, issba, deco) - render_dot_maybe(dotsrc.str(), dont_run_dot) + render_dot_maybe(dotsrc.str().encode('utf-8'), dont_run_dot) def render_formula(f): dotsrc = spot.ostringstream() @@ -251,35 +280,28 @@ def render_formula(f): def print_stats(automaton): stats = spot.stats_reachable(automaton) - print "

", stats.states, - if stats.states <= 1: - print " state,", - else: - print " states,", - print stats.transitions, - if stats.transitions <= 1: - print " transition,", - else: - print " transitions,", - # compute the number of acceptance conditions + unbufprint("

%d state" % stats.states) + if stats.states > 1: + unbufprint("s") + unbufprint(", %d transition" % stats.transitions) + if stats.transitions > 1: + unbufprint("s") count = automaton.number_of_acceptance_conditions() if count > 0: - print count, - if count <= 1: - print "acceptance condition:", - else: - print "acceptance conditions:", + unbufprint(", %d acceptance condition" % count) + if count > 1: + unbufprint("s") acc = automaton.all_acceptance_conditions() - print spot.bdd_format_accset(automaton.get_dict(), acc) + unbufprint(": " + spot.bdd_format_accset(automaton.get_dict(), acc)) else: - print "no acceptance condition (all cycles are accepting)" - print "

" + unbufprint(", no acceptance condition (all cycles are accepting)") + unbufprint("

\n") # Decide whether we will render the automaton or not. # (A webserver is not a computation center...) if stats.states > 64: return "Automaton has too much states" if float(stats.transitions)/stats.states > 10: - return "Automaton has too much transitions per states" + return "Automaton has too much transitions per state" return False form = cgi.FieldStorage() @@ -288,7 +310,7 @@ output_type = form.getfirst('o', 'v'); # Version requested. if output_type == 'v': - print 'Spot version ' + spot.version() + unbufprint('Spot version %s\n' % spot.version()) finish() spot.unblock_signal(signal.SIGALRM) @@ -304,9 +326,13 @@ pel = spot.empty_parse_error_list() f = spot.parse(formula, pel, env) if pel: - print '
' + unbufprint('
') err = spot.format_parse_errors(spot.get_cout(), formula, pel) - print '
' + unbufprint('
') + +# Do not continue if we could not parse anything sensible. +if not f: + finish() # Formula simplifications opt = spot.Reduce_None @@ -328,12 +354,11 @@ if opt != spot.Reduce_None: if output_type == 'f': formula_format = form.getfirst('ff', 'o') # o = Spot, i = Spin, g = GraphViz - if formula_format == 'o': - print '
%s
' % f + unbufprint('
%s
' % f) elif formula_format == 'i': - print ('
' - + spot.to_spin_string(f) + '
') + unbufprint('
' + + spot.to_spin_string(f) + '
') elif formula_format == 'g': render_formula(f) finish() @@ -377,9 +402,9 @@ issba = False if output_type == 'm': automaton = spot.scc_filter(automaton) automaton = spot.minimize_monitor(automaton) - print '
' + unbufprint('
') dont_run_dot = print_stats(automaton) - print '
' + unbufprint('
') render_automaton(automaton, dont_run_dot, issba) automaton = 0 finish() @@ -398,7 +423,7 @@ if output_type == 'a': elif output_type == 'r': buchi_type = form.getfirst('ra', 't') else: - print "Unkown output type 'o=%s'." % output_type + unbufprint("Unkown output type 'o=%s'.\n" % output_type) automaton = 0 finish() @@ -435,7 +460,7 @@ if output_type == 'a': if buchi_type == 'i': s = spot.ostringstream() spot.never_claim_reachable(s, degen, f) - print '
%s
' % cgi.escape(s.str()) + unbufprint('
%s
' % cgi.escape(s.str())) del s else: # 't' or 's' dont_run_dot = print_stats(degen) @@ -462,20 +487,28 @@ if output_type == 'r': eci, err = spot.emptiness_check_instantiator.construct(opt) if not eci: - print ('
Cannot parse "' + opt + '" near "' - + err + '".
') + unbufprint('
Cannot parse "' + opt + + '" near "' + err + '".
') else: ec_a = 0 n_acc = degen.number_of_acceptance_conditions() n_max = eci.max_acceptance_conditions() + n_min = eci.min_acceptance_conditions() if (n_acc <= n_max): - ec_a = degen + if (n_acc >= n_min): + ec_a = degen + else: + unbufprint('
Cannot run ' + opt + + ' on automata with less than ' + str(n_min) + + ' acceptance condition.
Please build ' + + 'a degeneralized Büchi automaton if you ' + + 'want to try this algorithm.
') else: - print ('
Cannot run ' + opt - + ' on automata with more than ' + str(n_max) - + ' acceptance condition.
Please build ' - + 'a degeneralized Büchi automaton if you ' - + 'want to try this algorithm.
') + unbufprint('
Cannot run ' + opt + + ' on automata with more than ' + str(n_max) + + ' acceptance condition.
Please build ' + + 'a degeneralized Büchi automaton if you ' + + 'want to try this algorithm.
') if ec_a: ec = eci.instantiate(ec_a) else: @@ -484,15 +517,16 @@ if output_type == 'r': if ec: ec_res = ec.check() if not ec_res: - print '
No accepting run found.
' + unbufprint('
No accepting run found.
') else: ec_run = ec_res.accepting_run() - print '
An accepting run was found.
' + unbufprint('
An accepting run was found.
') if ec_run: if print_acc_run: s = spot.ostringstream() spot.print_tgba_run(s, ec_a, ec_run) - print '
%s
' % cgi.escape(s.str()) + unbufprint('
%s
' % + cgi.escape(s.str())) del s if draw_acc_run: @@ -502,7 +536,7 @@ if output_type == 'r': del deco del ec_run del ec_res - print '
' + unbufprint('
') del ec del ec_a degen = 0 diff --git a/wrap/python/buddy.i b/wrap/python/buddy.i index 1f44a5197..e9fc2dd35 100644 --- a/wrap/python/buddy.i +++ b/wrap/python/buddy.i @@ -1,6 +1,8 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de l'EPITA. +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'EPITA. // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -224,11 +226,17 @@ extern const bdd bddtrue; #define BDD_REORDER_RANDOM 7 %extend bdd { - int - __cmp__(bdd* b) - { - return b->id() - self->id(); - } + // For Python 2.0 + int __cmp__(bdd* b) { return b->id() - self->id(); } + + // For Python 2.1+ and Python 3 + bool __le__(bdd* b) { return self->id() <= b->id(); } + bool __lt__(bdd* b) { return self->id() < b->id(); } + bool __eq__(bdd* b) { return self->id() == b->id(); } + bool __ne__(bdd* b) { return self->id() != b->id(); } + bool __ge__(bdd* b) { return self->id() >= b->id(); } + bool __gt__(bdd* b) { return self->id() > b->id(); } + std::string __str__(void) diff --git a/wrap/python/spot.i b/wrap/python/spot.i index b33534b51..271e8f572 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -1,9 +1,9 @@ - -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- encoding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012 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), -// Université Pierre et Marie Curie. +// de Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -114,6 +114,11 @@ using namespace spot; "$result = t_output_helper($result, SWIG_FromCharPtr(*$1));"; %apply char** OUTPUT { char** err }; +// False and True cannot be redefined in Python3, even in a class. +// Spot uses these in an enum of the constant class. +%rename(FalseVal) False; +%rename(TrueVal) True; + %include "misc/version.hh" %include "misc/bddalloc.hh" %include "misc/minato.hh" @@ -203,11 +208,23 @@ using namespace spot; // When comparing formula, make sure Python compare our // pointers, not the pointers to its wrappers. - int - __cmp__(const spot::ltl::formula* b) - { - return b - self; - } + + // __cmp__ is for Python 2.0 + int __cmp__(const spot::ltl::formula* b) { return self - b; } + // These are for Python 2.1+ or 3.x. They more closely match + // the logic in Spot. + bool __lt__(const spot::ltl::formula* b) + { spot::ltl::formula_ptr_less_than lt; return lt(self, b); } + bool __le__(const spot::ltl::formula* b) + { spot::ltl::formula_ptr_less_than lt; return !lt(b, self); } + bool __eq__(const spot::ltl::formula* b) { return self == b; } + bool __ne__(const spot::ltl::formula* b) { return self != b; } + bool __gt__(const spot::ltl::formula* b) + { spot::ltl::formula_ptr_less_than lt; return lt(b, self); } + bool __ge__(const spot::ltl::formula* b) + { spot::ltl::formula_ptr_less_than lt; return !lt(self, b); } + + size_t __hash__() { return self->hash(); } std::string __str__(void) @@ -265,12 +282,24 @@ get_cout() return std::cout; } +void +nl_cout() +{ + std::cout << std::endl; +} + std::ostream& get_cerr() { return std::cerr; } +void +nl_cerr() +{ + std::cerr << std::endl; +} + void print_on(std::ostream& on, const std::string& what) { diff --git a/wrap/python/tests/bddnqueen.py b/wrap/python/tests/bddnqueen.py index 12209fb11..3df597669 100755 --- a/wrap/python/tests/bddnqueen.py +++ b/wrap/python/tests/bddnqueen.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement -# de l'EPITA. +# Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +# Développement de l'EPITA. # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université # Pierre et Marie Curie. @@ -27,6 +27,7 @@ import sys from buddy import * +from spot import nl_cout # Build the requirements for all other fields than (i,j) assuming # that (i,j) has a queen. @@ -89,15 +90,15 @@ for i in side: # Build requirements for each variable(field). for i in side: for j in side: - print "Adding position %d, %d" % (i, j) + sys.stdout.write("Adding position %d, %d\n" % (i, j)) build(i, j) # Print the results. -print "There are", bdd_satcount(queen), "solutions" -print "one is:" +sys.stdout.write("There are %d solutions, one is:\n" % + bdd_satcount(queen)) solution = bdd_satone(queen) bdd_printset(solution) -print +nl_cout() # Cleanup all BDD variables before calling bdd_done(), otherwise # bdd_delref will be called after bdd_done() and this is unsafe in diff --git a/wrap/python/tests/interdep.py b/wrap/python/tests/interdep.py index 87dfacad5..ea6c7c738 100755 --- a/wrap/python/tests/interdep.py +++ b/wrap/python/tests/interdep.py @@ -1,7 +1,9 @@ -# -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2003, 2004, 2010 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement +# de l'EPITA. +# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 +# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +# Pierre et Marie Curie. # # This file is part of Spot, a model checking library. # @@ -24,6 +26,7 @@ # are not problematic. import buddy import spot +import sys e = spot.default_environment.instance() p = spot.empty_parse_error_list() f = spot.parse('GFa', p, e) @@ -31,13 +34,13 @@ dict = spot.bdd_dict() a = spot.ltl_to_tgba_lacim(f, dict) s0 = a.get_init_state() b = s0.as_bdd() -print b +sys.stdout.write("%s\n" % b) iter = a.succ_iter(s0) iter.first() while not iter.done(): c = iter.current_condition() - print c + sys.stdout.write("%s\n" % c) b &= c # `&=' is defined only in buddy. So if this statement works # it means buddy can grok spot's objects. iter.next() -print b +sys.stdout.write("%s\n" % b) diff --git a/wrap/python/tests/ltl2tgba.py b/wrap/python/tests/ltl2tgba.py index d8f07a7fe..bc9e46734 100755 --- a/wrap/python/tests/ltl2tgba.py +++ b/wrap/python/tests/ltl2tgba.py @@ -1,8 +1,8 @@ -# -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # # This file is part of Spot, a model checking library. @@ -30,7 +30,7 @@ import getopt import spot def usage(prog): - print "Usage: ", prog, """ [OPTIONS...] formula + sys.stderr.write("""Usage: %s [OPTIONS...] formula Options: -a display the acceptance_conditions BDD, not the reachability graph @@ -41,7 +41,8 @@ Options: -r display the relation BDD, not the reachability graph -R same as -r, but as a set -t display reachable states in LBTT's format - -v display the BDD variables used by the automaton""" + -v display the BDD variables used by the automaton +""" % prog) sys.exit(2) @@ -122,12 +123,12 @@ if f: if concrete: spot.bdd_print_set(cout, concrete.get_dict(), concrete.get_core_data().relation) - print + spot.nl_cout() elif output == 4: if concrete: spot.bdd_print_set(cout, concrete.get_dict(), concrete.get_core_data().acceptance_conditions) - print + spot.nl_cout() elif output == 5: a.get_dict().dump(cout) elif output == 6: diff --git a/wrap/python/tests/ltlparse.py b/wrap/python/tests/ltlparse.py index e67c64557..a8d953332 100755 --- a/wrap/python/tests/ltlparse.py +++ b/wrap/python/tests/ltlparse.py @@ -1,8 +1,8 @@ -# -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # # This file is part of Spot, a model checking library. @@ -36,12 +36,12 @@ for str1 in l: sys.exit(1) str2 = str(f) f.destroy() - print str2 + sys.stdout.write(str2 + "\n") # Try to reparse the stringified formula f = spot.parse(str2, p, e) if spot.format_parse_errors(spot.get_cout(), str2, p): sys.exit(1) - print f + sys.stdout.write(str(f) + "\n") f.destroy() assert spot.atomic_prop.instance_count() == 0 diff --git a/wrap/python/tests/ltlsimple.py b/wrap/python/tests/ltlsimple.py index 6091f7881..aa39c75ed 100755 --- a/wrap/python/tests/ltlsimple.py +++ b/wrap/python/tests/ltlsimple.py @@ -1,8 +1,8 @@ -# -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # # This file is part of Spot, a model checking library. @@ -23,6 +23,7 @@ # 02111-1307, USA. import spot +import sys e = spot.default_environment.instance() @@ -42,18 +43,18 @@ op2 = spot.multop.instance(spot.multop.And, op, c) # suppressed, so we don't attempt to reuse it elsewhere. del op, c -print 'op2 =', op2 +sys.stdout.write('op2 = %s\n' % str(op2)) op3 = spot.multop.instance(spot.multop.And, b, - spot.multop.instance(spot.multop.And, c2, a)) + spot.multop.instance(spot.multop.And, c2, a)) del a, b, c2 -print 'op3 =', op3 +sys.stdout.write('op3 = %s\n' % str(op3)) assert op2 == op3 op4 = spot.multop.instance(spot.multop.Or, op2, op3) -print 'op4 =', op4 +sys.stdout.write('op4 = %s\n' % str(op4)) assert op4 == op2 del op2, op3 diff --git a/wrap/python/tests/minato.py b/wrap/python/tests/minato.py index 71b1bdd9d..247cea2be 100755 --- a/wrap/python/tests/minato.py +++ b/wrap/python/tests/minato.py @@ -1,6 +1,8 @@ -# -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2004, 2010 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement +# de l'Epita +# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # # This file is part of Spot, a model checking library. @@ -40,7 +42,7 @@ i = isop.next() l = [] while i != buddy.bddfalse: buddy.bdd_printset(i) - print + spot.nl_cout() l.append(i) i = isop.next() diff --git a/wrap/python/tests/modgray.py b/wrap/python/tests/modgray.py index 72ba1d5d2..6430d0451 100755 --- a/wrap/python/tests/modgray.py +++ b/wrap/python/tests/modgray.py @@ -1,6 +1,8 @@ -# -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2004, 2010 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement +# de l'Epita. +# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # # This file is part of Spot, a model checking library. @@ -21,6 +23,7 @@ # 02111-1307, USA. import spot +import sys class test(spot.loopless_modular_mixed_radix_gray_code): def __init__(self, lim): @@ -43,7 +46,7 @@ class test(spot.loopless_modular_mixed_radix_gray_code): while not self.done(): m = "".join(self.msg) res.append(m) - print m + sys.stdout.write(m + "\n") self.next() return res diff --git a/wrap/python/tests/optionmap.py b/wrap/python/tests/optionmap.py index 066edb5f8..73d8cf052 100755 --- a/wrap/python/tests/optionmap.py +++ b/wrap/python/tests/optionmap.py @@ -1,6 +1,8 @@ -# -*- mode: python; coding: iso-8859-1 -*- -# Copyright (C) 2005, 2010 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement +# de l'EPITA. +# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # # This file is part of Spot, a model checking library. @@ -47,17 +49,13 @@ assert o.get('optB') == 0 assert o.get('optC') == 1 res = o.parse_options("!") -print res assert res == "!" res = o.parse_options("foo, !opt = 1") -print res assert res == "!opt = 1" res = o.parse_options("foo=3, opt == 1") -print res assert res == "opt == 1" res = o.parse_options("foo=3opt == 1") -print res assert res == "3opt == 1"