Difference between revisions of "Maude Tools:Order-sorted Term Patterns"
Maudesystem (Talk | contribs) (Created page with "== Introduction == This page introduces the Maude Order-sorted Pattern Solver, a tool that accepts an order-sorted pattern as input and can—in many...") |
Maudesystem (Talk | contribs) |
||
(15 intermediate revisions by the same user not shown) | |||
Line 1: | Line 1: | ||
== Introduction == | == Introduction == | ||
− | This page introduces the [[The Maude System|Maude]] Order-sorted Pattern | + | This page introduces the [[The Maude System|Maude]] Order-sorted Pattern Tool. The tool has two primary functions: |
− | + | ||
+ | # Given an order-sorted signature and a sort, it can check if the sort is finite or empty. Further, it can generate the set of all terms inside a finite sort. | ||
+ | # Given an order-sorted signature and an order-sorted pattern (syntax shown below), it can—in many cases—discover a finite union of terms equivalent to the given pattern, if it exists. | ||
Order-sorted term patterns are a simple notation for describing unions, intersections, and differences of sets of terms generated by an order-sorted signature. | Order-sorted term patterns are a simple notation for describing unions, intersections, and differences of sets of terms generated by an order-sorted signature. | ||
Line 13: | Line 15: | ||
Suppose <tt>t1</tt>, <tt>t2</tt>, and <tt>t3</tt> are terms in an order-sorted signature. Then: | Suppose <tt>t1</tt>, <tt>t2</tt>, and <tt>t3</tt> are terms in an order-sorted signature. Then: | ||
− | # <tt>{t1 | + | # <tt>{t1} U {t2} U {t3}</tt> is the pattern representing the union of instances these terms. |
# <tt>{t1} - {t2}</tt> is the pattern representing the instances of <tt>t1</tt> that are not instances of <tt>t2</tt>. | # <tt>{t1} - {t2}</tt> is the pattern representing the instances of <tt>t1</tt> that are not instances of <tt>t2</tt>. | ||
− | # <tt>{t1 | + | # <tt>({t1} U {t2}) & {t3}</tt> is the pattern representing the intersection of instances of <tt>t1</tt> and <tt>t2</tt> with <tt>t3</tt>. |
+ | # <tt>mt</tt> is the empty pattern which has no instances. | ||
− | == Theoretical Details == | + | == Theoretical Details of Sort Operations == |
+ | |||
+ | === Sort Emptiness === | ||
+ | |||
+ | Checking sort emptiness can be be reduced to a rewrite system reachability problem over finite sets of sorts in the original signature | ||
+ | where: | ||
+ | |||
+ | # For each non-constant operator <tt>f : s1 ... sn -> s</tt>, we add a rule <tt>s -> s1 ... sn</tt> | ||
+ | # For each constant operator <tt> c : -> s</tt>, we add a rule <tt>s -> *</tt> | ||
+ | # For each subsort inclusion <tt> s < s'</tt>, we add a rule <tt>s' -> s</tt> | ||
+ | # The reachability problem in question is given by <tt> s ->+ *</tt> | ||
+ | |||
+ | === Sort Finiteness === | ||
+ | |||
+ | Checking sort finiteness can be reduced to an LTL model checking problem where: | ||
+ | |||
+ | # The LTL model states are the sorts in the original signature | ||
+ | # For each sort <tt>s</tt>, we have label <tt>@(s)</tt> which holds iff the current state is <tt>s</tt> | ||
+ | # For each operator <tt>f : s1 ... sn -> s</tt> where input sorts are non-empty and sort <tt>s'</tt> where <tt>s < s'</tt>, add rules <tt>s -> si</tt> for each <tt>1 <= i <= n</tt> | ||
+ | # Each sort with no constructible terms besides constants is called a <tt>final sort</tt>; for each final sort <tt>s</tt> add a rule <tt>s -> s</tt> | ||
+ | # Then, to prove a given sort <tt>s</tt> is finite, for each non-final sort <tt>s'</tt> reachable from <tt>s</tt>, check that <tt>s'</tt> cannot reach itself (this proposition is expressible as an LTL formula) | ||
+ | |||
+ | == Theoretical Details of Pattern Operations == | ||
=== Closure Under Boolean Operations === | === Closure Under Boolean Operations === | ||
− | For some signatures, term patterns are closed under union, intersection, and difference. Otherwise, we can usually apply a transformation to a signature so that it | + | For some order-sorted signatures, term patterns are closed under union, intersection, and difference. Otherwise, we can usually apply a transformation to a signature so that it |
becomes closed under these operations. | becomes closed under these operations. | ||
Line 47: | Line 72: | ||
== Download == | == Download == | ||
− | + | To use the pattern solver tool, both of the following tarballs will need to be downloaded. | |
+ | Note that currently, the binary is compiled for Linux only. Any modern Linux distribution should be unproblematic. | ||
+ | |||
+ | [http://maude.cs.illinois.edu/tools/term-patterns/maude2.7-bin.tar.gz Maude 2.7 rewrite engine download] | ||
+ | |||
+ | [http://maude.cs.illinois.edu/tools/term-patterns/pat-solve-rel.tar.gz Pattern Solver download] | ||
+ | |||
+ | Once you have downloaded and unpacked both archives, you can run examples. To do so, you need to invoke the | ||
+ | Maude rewrite engine (called <tt>maude</tt> in Maude binary tarball) on the example you wish to run. | ||
+ | For example, if I unpacked both archives in my home directory and wanted to run the Pichler example (shown below), | ||
+ | I could run: | ||
+ | |||
+ | <tt># ~/maude2.7-bin/maude ~/pat-solve-rel/examples/pichler-ex.maude</tt> | ||
== Tool Example Inputs == | == Tool Example Inputs == | ||
− | + | The following example inputs are all taken from the /examples folder inside the root directory of the pattern solver tool: | |
+ | |||
+ | # [http://maude.cs.illinois.edu/tools/term-patterns/pichler-ex.maude Pichler Example] | ||
+ | # [http://maude.cs.illinois.edu/tools/term-patterns/succ-ex1.maude Successor Example] | ||
+ | # [http://maude.cs.illinois.edu/tools/term-patterns/simple-diff2.maude Simple Difference Example] | ||
+ | |||
+ | These examples are all formatted as equalities between two pattern terms, tested using the method presented above. | ||
+ | The terms occurring in a pattern are presented using Maude META-LEVEL syntax, which is documented in the | ||
+ | [http://maude.cs.illinois.edu/w/images/1/1a/Maude-manual.pdf Maude Manual] (see section 11.2). | ||
+ | |||
+ | Hopefully, the examples will give a flavor of how the syntax looks when written down and the kinds of queries one might make. | ||
+ | |||
+ | == Papers == | ||
+ | |||
+ | Paper download links coming soon. |
Latest revision as of 18:49, 22 October 2015
Contents
Introduction
This page introduces the Maude Order-sorted Pattern Tool. The tool has two primary functions:
- Given an order-sorted signature and a sort, it can check if the sort is finite or empty. Further, it can generate the set of all terms inside a finite sort.
- Given an order-sorted signature and an order-sorted pattern (syntax shown below), it can—in many cases—discover a finite union of terms equivalent to the given pattern, if it exists.
Order-sorted term patterns are a simple notation for describing unions, intersections, and differences of sets of terms generated by an order-sorted signature.
Our tool transforms general patterns into finite unions by interpreting intersection as unification and difference as an application of our order-sorted symbolic difference algorithm.
Example Patterns
Suppose t1, t2, and t3 are terms in an order-sorted signature. Then:
- {t1} U {t2} U {t3} is the pattern representing the union of instances these terms.
- {t1} - {t2} is the pattern representing the instances of t1 that are not instances of t2.
- ({t1} U {t2}) & {t3} is the pattern representing the intersection of instances of t1 and t2 with t3.
- mt is the empty pattern which has no instances.
Theoretical Details of Sort Operations
Sort Emptiness
Checking sort emptiness can be be reduced to a rewrite system reachability problem over finite sets of sorts in the original signature where:
- For each non-constant operator f : s1 ... sn -> s, we add a rule s -> s1 ... sn
- For each constant operator c : -> s, we add a rule s -> *
- For each subsort inclusion s < s', we add a rule s' -> s
- The reachability problem in question is given by s ->+ *
Sort Finiteness
Checking sort finiteness can be reduced to an LTL model checking problem where:
- The LTL model states are the sorts in the original signature
- For each sort s, we have label @(s) which holds iff the current state is s
- For each operator f : s1 ... sn -> s where input sorts are non-empty and sort s' where s < s', add rules s -> si for each 1 <= i <= n
- Each sort with no constructible terms besides constants is called a final sort; for each final sort s add a rule s -> s
- Then, to prove a given sort s is finite, for each non-final sort s' reachable from s, check that s' cannot reach itself (this proposition is expressible as an LTL formula)
Theoretical Details of Pattern Operations
Closure Under Boolean Operations
For some order-sorted signatures, term patterns are closed under union, intersection, and difference. Otherwise, we can usually apply a transformation to a signature so that it becomes closed under these operations.
Special Patterns
Assuming finite signatures, there is a finite pattern which generates every term. There is also a finite pattern generates no terms (e.g. the empty pattern).
Pattern Equivalence
Two patterns are considered equivalent if they generate the same term set. This condition can be checked by observing if the subtracting each pattern by the other results in the empty pattern.
Relationship to Propositional Tree Automata
An order-sorted signature can be viewed as a tree automaton that accepts as inputs any term that the signature generates. The generalization of a tree automaton—a propositional tree automaton—can accept not only terms but also unions, intersections, and complements of terms. Our order-sorted term patterns provide a simpler and more intuitive algorithm which accomplishes this same task.
Order-sorted Symbolic Difference
Our symbolic difference algorithm generalizes previous approaches such as that of Lassez and Marriott, by extending to the case of order-sorted terms.
Download
To use the pattern solver tool, both of the following tarballs will need to be downloaded. Note that currently, the binary is compiled for Linux only. Any modern Linux distribution should be unproblematic.
Maude 2.7 rewrite engine download
Once you have downloaded and unpacked both archives, you can run examples. To do so, you need to invoke the Maude rewrite engine (called maude in Maude binary tarball) on the example you wish to run. For example, if I unpacked both archives in my home directory and wanted to run the Pichler example (shown below), I could run:
# ~/maude2.7-bin/maude ~/pat-solve-rel/examples/pichler-ex.maude
Tool Example Inputs
The following example inputs are all taken from the /examples folder inside the root directory of the pattern solver tool:
These examples are all formatted as equalities between two pattern terms, tested using the method presented above. The terms occurring in a pattern are presented using Maude META-LEVEL syntax, which is documented in the Maude Manual (see section 11.2).
Hopefully, the examples will give a flavor of how the syntax looks when written down and the kinds of queries one might make.
Papers
Paper download links coming soon.