Showing
5 changed files
with
67 additions
and
27 deletions
This diff is collapsed. Click to expand it.
1 | -"""A module to save and load objects in PNML. | 1 | +"""This module allows to save and load objects in PNML. The standard |
2 | - | 2 | +is correctly handled for low-level nets, ie, nets with only `True` |
3 | -Petri nets objects are saved in PNML, other Python objects are saved | 3 | +guards and black tokens. However, module `snakes.pnml` was actually |
4 | -in a readable format when possible and pickled as a last solution. | 4 | +created long before the PNML standard was extended to handle |
5 | -This should result in a complete PNML serialization of any object. | 5 | +high-level nets (in particular coloured variants) and so the standard |
6 | - | 6 | +is not respected in this case. Consequently, in the following, we |
7 | -@todo: revise documentation | 7 | +abuse the term PNML for the XML produced and read by SNAKES. |
8 | + | ||
9 | +@warning: this module will be replaced in a future version of SNAKES, | ||
10 | + so its documentation will be kept minimal. | ||
8 | """ | 11 | """ |
9 | 12 | ||
10 | import xml.dom.minidom | 13 | import xml.dom.minidom |
... | @@ -160,6 +163,7 @@ class _set (object) : | ... | @@ -160,6 +163,7 @@ class _set (object) : |
160 | """ | 163 | """ |
161 | return len(self._data) | 164 | return len(self._data) |
162 | 165 | ||
166 | +# apidoc skip | ||
163 | class Tree (object) : | 167 | class Tree (object) : |
164 | """Abstraction of a PNML tree | 168 | """Abstraction of a PNML tree |
165 | 169 | ||
... | @@ -911,7 +915,9 @@ class Tree (object) : | ... | @@ -911,7 +915,9 @@ class Tree (object) : |
911 | raise SnakesError("unsupported PNML tag '%s'" % self.name) | 915 | raise SnakesError("unsupported PNML tag '%s'" % self.name) |
912 | 916 | ||
913 | def dumps (obj) : | 917 | def dumps (obj) : |
914 | - """Dump an object to a PNML string | 918 | + """Dump an object to a PNML string, any Python object may be |
919 | + serialised this way (resorting to pickling when the object does | ||
920 | + not support serialisation to PNML). | ||
915 | 921 | ||
916 | >>> print(dumps(42)) | 922 | >>> print(dumps(42)) |
917 | <?xml version="1.0" encoding="utf-8"?> | 923 | <?xml version="1.0" encoding="utf-8"?> | ... | ... |
... | @@ -24,9 +24,9 @@ at SNAKES source code. However, let's note a few points: | ... | @@ -24,9 +24,9 @@ at SNAKES source code. However, let's note a few points: |
24 | * most Epydoc fields are supported: `@param`, `@type`, `@note`, ... | 24 | * most Epydoc fields are supported: `@param`, `@type`, `@note`, ... |
25 | * directive `# apidoc skip` allow not to include the next object in | 25 | * directive `# apidoc skip` allow not to include the next object in |
26 | the generated documentation | 26 | the generated documentation |
27 | - * directive `apidoc stop` allow to stop the processing of current | 27 | + * directive `# apidoc stop` allow to stop the processing of current |
28 | object (module or class) | 28 | object (module or class) |
29 | - * directive `apidoc include 'filename' lang='language'` allow to | 29 | + * directive `# apidoc include 'filename' lang='language'` allow to |
30 | include the content of a file as a block of source code in the | 30 | include the content of a file as a block of source code in the |
31 | specified language | 31 | specified language |
32 | * when statement `pass` is found in a doctest, the rest of the | 32 | * when statement `pass` is found in a doctest, the rest of the |
... | @@ -38,11 +38,12 @@ at SNAKES source code. However, let's note a few points: | ... | @@ -38,11 +38,12 @@ at SNAKES source code. However, let's note a few points: |
38 | options nor customisation, however, it is quite flexible already | 38 | options nor customisation, however, it is quite flexible already |
39 | by the way it handles documentation | 39 | by the way it handles documentation |
40 | 40 | ||
41 | -@note: we do not build doc for the sub-modules of `snakes.lang` | 41 | +@note: in the example above we do not build doc for the sub-modules of |
42 | - because some of them are programmed for distinct versions of | 42 | + `snakes.lang` because some of them are programmed for distinct |
43 | - Python with incompatible syntaxes. So `apidoc` will fail for sure | 43 | + versions of Python with incompatible syntaxes. So `apidoc` will |
44 | - on one or another of these modules. Fortunately, most of the | 44 | + fail for sure on one or another of these modules. Fortunately, |
45 | - documentation for `snakes.lang` is in the package itself. | 45 | + most of the documentation for `snakes.lang` is in the package |
46 | + itself. | ||
46 | @note: for better rendering, `apidoc` uses [Python | 47 | @note: for better rendering, `apidoc` uses [Python |
47 | Markdown](http://pythonhosted.org/Markdown), however, it will | 48 | Markdown](http://pythonhosted.org/Markdown), however, it will |
48 | handle situations when it is not installed | 49 | handle situations when it is not installed |
... | @@ -578,10 +579,11 @@ class DocExtract (object) : | ... | @@ -578,10 +579,11 @@ class DocExtract (object) : |
578 | for exc, reason in sorted(info["raise"].items()) : | 579 | for exc, reason in sorted(info["raise"].items()) : |
579 | self.writelist("`%s`: %s" % (exc, reason)) | 580 | self.writelist("`%s`: %s" % (exc, reason)) |
580 | self.newline() | 581 | self.newline() |
581 | - def write_include (self, name, lang="python") : | 582 | + def write_include (self, name, lang="python", first=1, last=-1) : |
582 | """Write a block of source code included through directive | 583 | """Write a block of source code included through directive |
583 | `apidoc include ...` | 584 | `apidoc include ...` |
584 | """ | 585 | """ |
586 | + first, last = int(first), int(last) | ||
585 | if os.path.exists(name) : | 587 | if os.path.exists(name) : |
586 | path = name | 588 | path = name |
587 | else : | 589 | else : |
... | @@ -591,8 +593,9 @@ class DocExtract (object) : | ... | @@ -591,8 +593,9 @@ class DocExtract (object) : |
591 | with open(path) as infile : | 593 | with open(path) as infile : |
592 | self.newline() | 594 | self.newline() |
593 | self.writeline(" :::%s" % lang) | 595 | self.writeline(" :::%s" % lang) |
594 | - for line in infile : | 596 | + for i, line in enumerate(infile) : |
595 | - self.writeline(" " + line.rstrip()) | 597 | + if first <= i+1 and (last == -1 or i+1 <= last) : |
598 | + self.writeline(" " + line.rstrip()) | ||
596 | self.newline() | 599 | self.newline() |
597 | 600 | ||
598 | def main (finder, args, source=None) : | 601 | def main (finder, args, source=None) : | ... | ... |
1 | +"""This module features a parser for CTL* formula. Function `build` | ||
2 | +parses the formula (see _concrete syntax_ below) and expands | ||
3 | +sub-formulas; then it returns an abstract syntax tree (see _abstract | ||
4 | +syntax_) below. | ||
5 | + | ||
6 | +>>> from snakes.utils.ctlstar.build import * | ||
7 | +>>> spec = ''' | ||
8 | +... atom even (x : int) : | ||
9 | +... return x % 2 == 0 | ||
10 | +... atom odd (x : int) : | ||
11 | +... return x % 2 == 1 | ||
12 | +... prop evenplace (p : place) : | ||
13 | +... exists tok in p (even(x=tok)) | ||
14 | +... prop oddplace (p : place) : | ||
15 | +... exists tok in p (odd(x=tok)) | ||
16 | +... A (G (evenplace(p=@'some_place') => F oddplace(p=@'another_place'))) | ||
17 | +... ''' | ||
18 | +>>> tree = build(spec) | ||
19 | +>>> print ast.dump(tree) | ||
20 | +CtlUnary(op=All(), child=CtlUnary(op=Globally(), child=CtlBinary(op=Imply(), ... | ||
21 | + | ||
22 | +In the example above, `atom` allows to define parameterised atomic | ||
23 | +propositions and `prop` allows to define sub-formulas. In the returned | ||
24 | +syntax tree, all these objects are inlined and fully instantiated. | ||
25 | + | ||
26 | +## Concrete syntax ## | ||
1 | """ | 27 | """ |
2 | -@todo: revise (actually make) documentation | 28 | + |
29 | +# apidoc include "../../lang/ctlstar/ctlstar.pgen" first=6 last=35 lang="text" | ||
30 | + | ||
3 | """ | 31 | """ |
32 | +## Abstract syntax ## | ||
33 | +""" | ||
34 | + | ||
35 | +# apidoc include "../../lang/ctlstar/ctlstar.asdl" first=3 last=59 lang="text" | ||
36 | +pass | ... | ... |
1 | from snakes.lang.ctlstar.parser import parse | 1 | from snakes.lang.ctlstar.parser import parse |
2 | from snakes.lang.ctlstar import asdl as ast | 2 | from snakes.lang.ctlstar import asdl as ast |
3 | -from snakes.lang import getvars, bind | 3 | +from snakes.lang import bind |
4 | import _ast | 4 | import _ast |
5 | 5 | ||
6 | class SpecError (Exception) : | 6 | class SpecError (Exception) : |
... | @@ -53,7 +53,7 @@ class Builder (object) : | ... | @@ -53,7 +53,7 @@ class Builder (object) : |
53 | node.atomic = (isinstance(node.op, ast.Not) | 53 | node.atomic = (isinstance(node.op, ast.Not) |
54 | and node.child.atomic) | 54 | and node.child.atomic) |
55 | else : | 55 | else : |
56 | - assert False, "how did we get there?" | 56 | + raise SpecError(node, "not a CTL* formula") |
57 | return node | 57 | return node |
58 | def _build_place (self, param, ctx) : | 58 | def _build_place (self, param, ctx) : |
59 | if isinstance(param, ast.Parameter) : | 59 | if isinstance(param, ast.Parameter) : |
... | @@ -144,9 +144,7 @@ class Builder (object) : | ... | @@ -144,9 +144,7 @@ class Builder (object) : |
144 | del new.params[:] | 144 | del new.params[:] |
145 | return new | 145 | return new |
146 | 146 | ||
147 | -def build (spec, main=None) : | 147 | +def build (spec) : |
148 | - b = Builder(spec) | 148 | + if isinstance(spec, str) : |
149 | - if main is None : | 149 | + spec = parse(spec) |
150 | - return b.build(spec.main) | 150 | + return Builder(spec).build(spec.main) |
151 | - else : | ||
152 | - return b.build(main) | ... | ... |
-
Please register or login to post a comment