Home

Grez – User Manual

Contents

1. Connect f w gt ee The numbers below the nodes indicate what nodes are mapped to each other by the correspondence morphism This graph transformation system is repre sented by the following SGF code Send rule 1 M gt 1 C gt 2 U gt 2 gt 1 C gt 2 M gt 2 Add rule 1 8 gt 1 C gt 2 S gt 2 gt 1 lt gt 1 C gt a 0 gt 2 S gt 2 n gt n gt Connect rule node 1 ft 8 gt 1 r gt 1 C gt n n gt n U gt n F AdHocRouting gts rules Send Add Connect 3 23 Five Theoretical Foundations In this chapter we present some of the theoretical foundations of the termination proving techniques used in Grez We have choses to keep the text on a high level referring to the literature for the details 5 1 Graph transformation Grez uses so called hypergraphs A hypergraph differs from a normal graph in that edges can be incident to any number of nodes Formally a hypergraph G consists of a finite set of nodes Ve sometimes also called vertices in the literature and a finite set of edges Eg disjoint from Vg Each edge e Eg has a label labg e and a sequence of incident nodes attg e C VZ Note that in this approach nodes do not have labels they solely serve as a means to connect edges In the following a hypergraph will be simply called a graph We will sometim
2. graph_desc 31 graph_desc y wpe The definition of graphs is the same as in 4 2 3 The correspondence morphism is automatically generated from the graph definitions by mapping each node and edge of the left hand side to the node or edge of the right hand side with the same name if it exists 4 2 6 Transformation systems A transformation system is a set of rules Trans formation systems are defined by the following grammar 21 4 SPECIFYING GRAPH TRANSFORMATION SYSTEMS THE SIMPLE GRAPH FORMAT gts gt gts rules rules pel S a rules rule ref rule_ref rule_ref rule name The list of rules is a comma separated list in which each entry is an in place rule definition the non terminal rule is defined in 4 2 5 or the name of a previously defined rule 4 3 Examples 4 3 1 Two systems in one file It is possible to define two or more graph trans formation systems in a single SGF file This can be useful if the two systems share certain graphs or rules For example A B graph 1 A gt 2 graph 1 B gt 2 AtoB rule left A right B morphism 1 gt 1 2 gt 2 morphism BtoA rule left B right A morphism 1 gt 1 2 gt 2 morphism SysAtoB rules gts 1 AtoB 22 SysBtoA gts rules BtoA Es SysAeqB gts rules AtoB BtoA F3 If the user tries t
3. algos list Select the algorithm s to try List is a comma separated list of algo rithms see 3 3 threads num Specify the number of worker threads that Grez uses when executing the Prove or Compare actions The default value is the number of separate CPU cores in the machine The Trace action uses a single thread regardless of the value of this parameter system system If the input file contains more than one graph transformation system select the one with the given name random Generate a random graph transfor mation system beta Enable algorithms that are based on unpublished results and or currently in beta stage These algorithms are disabled by default Note that these algorithms are not documented 3 2 3 Reporting and proof generation progress style Set the progress report style possibilities for style are silent no progress report nice the default nice unicode and standard rtype ert Set the file type of the gener ated report proof disproof possibilities for ext are silent do not write report text text only default and pdf PDF For the last option a IATEX distribution is required 14 rfile file Set the file where the generated report is written default is standard out if rtype text and grez output pdf if rtype pdf silent Shorthand for rftype silent progress silent 3 2 4 Random system generation For more information
4. 1 5 one can also use in any directory the following grez cli lt args gt In both cases the lt args gt consist of a number of command line options and optionally a single input file An option starts with or and any other command line argument is interpreted as an file name The cli option makes sure that Grez s graphical user interface is not started The command line options and input file may occur in any order The available command line options are listed in the next section 3 2 Command line options Options start with or These three are equivalent for example help help and help are all recognized as a command line op tion and have the same effect The available command line options are 3 2 1 General options help h Display usage information basi cally the information of this section and abort version v Display version information and abort cli c Use the command line interface that is do not start the graphical user in terface If none of the above options are present the graphical user interface is started 13 3 THE COMMAND LINE INTERFACE 3 2 2 Action type and system selection action act Select the action to perform possibilities for act are prove try to prove termination or non termination of a graph transformation system compare compare results of different algorithms and trace produce a trace of a supported algorithm
5. Tries to prove termination by showing that the number of nodes de creases in each transformation step This algorithm is described in 5 4 2 PetriNet tool s Tries to prove termination by approximating the graph transformation system by a Petri net This algorithm is described in 5 4 4 This algorithm requires an external SMT solver the name of which is specified by the tool parameter TypeGraph smt b tool s nodes n max n wt s nrt b Tries to prove termina tion by the weighted type graph method described in 5 4 5 The parameters are smt whether or not to use an external SMT solver tool SMT solver to use only if SMT is used nodes maximum number of nodes in generated type graph max maximum weight of generated type graph only if SMT is not used wt evaluation type if it contains T tropical evaluation may be used if it contains A arctic evaluation can be used if it contains N arithmetic evaluation can be used nrt wether or not to use non relative termination This option is only available if an SMT solver is used 15 Four Specifying Graph Transformation Systems The Simple Graph Format Currently Grez does not provide a graphical user interface for constructing graph transformation systems It can generate random graph trans formation systems or read existing ones from a file stored on disk If the user wants to find a termination proof of a
6. discrete 14 h 13 help 13 if size 14 labels 15 left conn 14 left dens 14 left size 14 progress 14 random 14 rfile 14 right conn 14 43 right dens 14 right size 14 rtype 14 o rules 14 silent 14 system 5 7 14 threads 14 v 13 version 13 Compare action 9 Complete button 9 conservative minimization 30 copy textttcopy19 Cycle finder algorithm 27 cycle finder algorithm 15 Cycle finder algorithms 9 CycleFinder 15 Default button 9 double pushout approach 25 edge counter algorithm 10 15 28 edge counting 28 edge factorization 30 EdgeCounter 15 Edit button 9 Execute button Exit menu item External 15 external tool algorithm 10 15 6 6 from 20 Generate random GTS INDEX dialog 7 8 menu item 6 7 graph 25 graph 20 graph transformation rule see rule graph transformation system 26 graphical user interface 5 12 GTS see graph transformation system gts 18 21 GUI see graphical user interface GUI options menu item 6 Help menu 7 12 hypergraph see graph incident 25 incoming edge factorization see edge factor ization installation 2 main menu 5 6 main window 5 6 match bound algorithm 10 15 30 match bounds 29 30 MatchBound 15 morphism 25 morphism 20 Move down button 9 Move up button 9 name of Grez 1 node 18 20 node counter algorithm 10 15 28 node coun
7. gt wt mp The following termination argument was proved in 5 Theorem 5 4 4 Let T be a weighted type graph IfR and S are graph transformation systems such that all rules of R are tropically decreasing with respect to T and all rules of S are tropically non increasing with respect to T then RUS is terminating if and only if S is Arctic evaluation This termination technique was introduced in 5 It is very similar to the tropical evaluation except that rules are evaluated from left to right As the tropical evaluation this technique supports relative termination Given a weighted type graph T the weight of a morphism m G T is defined in the same way as with the tropical evaluation A rule p L R with correspondence mor phism f is called arcticly decreasing with respect to T if for each morphism mp R T there exists a morphism mz L gt T which agrees on f such that wt m gt wt mp it is called arcticly non increasing with respect to T if for each morphism mp R T there exists a mor phism mz L T which agrees on f such that wt m gt wt mp The following termination argument was proved in 5 Theorem 5 4 5 Let T be a weighted type graph If R and S are graph transformation systems such that all rules of R are arcticly decreasing with respect to T and all rules of S are arcticly non increasing with respect to T then RUS is terminating if and only if S is Arithmetical evaluation
8. This termination technique was introduced in 4 The technique supports relative termination 29 5 THEORETICAL FOUNDATIONS Given a weighted type graph 7 the weight of a graph G denoted wt G is the sum of the weights of all morphisms m G gt T denoted wt m which is the product of all the weights in its image Then a rule p L pr I r gt R with morphism f I gt T is called arithmetically non increasing with respect to T if for all f it holds that Ym Lor wt mL gt mp Ror wt mR MROPRZ MLOPL it is called arithmetically decreasing with respect to T if the sum of weights for mz is gt than the sum of weights for mp with respect to f I gt T where f maps all nodes onto the flower node of T The following termination argument was proved in 4 Theorem 5 4 6 Let T be a weighted type graph IFR and S are graph transformation systems such that all rules of R are arithmetically decreasing with respect to T and all rules of S are arith metically non increasing with respect to T then RUS is terminating if and only if S is 5 4 6 Match bounds The match bound technique implemented in Grez is a slightly improved version of the technique presented in 3 The idea is to annotate each edge with a match height informally the number of rule applications responsible for creating the edge in question If the match height of the graph transformation system is bounded then the graph transformation sy
9. loss of use data or profits or business interruption however caused and on any theory of liability whether in contract strict liability or tort including negligence or otherwise arising in any way out of the use of this software even if advised of the possibility of such damage A 2 Apache License version 2 0 1 Definitions License shall mean the terms and conditions for use reproduction and distri bution as defined by Sections 1 through 9 of this document Licensor shall mean the copyright owner or entity authorized by the copyright owner that is granting the License Legal Entity shall mean the union of the acting entity and all other entities that control are controlled by or are under common control with that entity For the purposes of this definition control means i the power direct or indirect to cause the direction or management of such entity whether by contract or otherwise or ii ownership of fifty percent 50 or more of the outstanding shares or iii beneficial ownership of such entity You or Your shall mean an individual or Legal Entity exercising permissions granted by this License Source form shall mean the preferred form for 33 A LICENSE TEXTS making modifications including but not limited to software source code documentation source and configuration files Object form shall mean any form resulting from mechanical transf
10. service marks or product names of the Licensor except as required for reasonable and custom ary use in describing the origin of the Work and reproducing the content of the NOTICE file 7 Disclaimer of Warranty Unless required by applicable law or agreed to in writing Licensor provides the Work and each Contributor provides its Contributions on an as is basis without warranties or conditions of any kind either ex press or implied including without limitation any warranties or conditions of title non infringement merchantability or fitness for a particular pur pose You are solely responsible for determining the appropriateness of using or redistributing the Work and assume any risks associated with Your exercise of permissions under this License 8 Limitation of Liability In no event and under no legal theory whether in tort includ ing negligence contract or otherwise unless required by applicable law such as deliberate and grossly negligent acts or agreed to in writing shall any Contributor be liable to You for damages including any direct indirect special incidental or consequential damages of any character arising as a result of this License or out of the use or in ability to use the Work including but not limited to damages for loss of goodwill work stoppage computer failure or malfunction or any and all other commercial damages or losses even if such Contributor has been advised of the poss
11. which associates a subset of the nodes and edges of the left hand side with nodes and edges of the right hand side There are two ways in which rules can be specified firstly the three components of a rule can be given explicitly and secondly there is a short hand form where the correspondence morphism is automatically constructed from the names of the nodes and edges of the left hand side and the right hand side In addition to these three components SGF allows the definition of negative application conditions Since they are ignored by Grez they are not described here rule exp_rule short_rule Explicit form In the explicit form a rule is defined by the following grammar rule left graph_ref right graph_ref morphism morph_ref graph_ref graph name morph_ref morphism name exp_rule The three components of a rule are explicitly spec ified either by referring by name to a previously defined graph or morphism or by defining the components in place the graph and morphism non terminals are defined in 4 2 3 and 4 2 4 respectively The left hand side right hand side and morphism can be given in any order and from their definition until the end of the rule declara tion scope left right and morphism function as names for the respective objects Short hand form In the short hand form a rule is defined by the following grammar short_rule gt rule
12. Licensed Material and in which the Licensed Material is translated altered arranged transformed or otherwise modified in a manner requiring permission un der the Copyright and Similar Rights held by the Licensor For purposes of this Public Li cense where the Licensed Material is a mu 36 sical work performance or sound recording Adapted Material is always produced where the Licensed Material is synched in timed relation with a moving image Adapter s License means the license You ap ply to Your Copyright and Similar Rights in Your contributions to Adapted Material in ac cordance with the terms and conditions of this Public License Copyright and Similar Rights means copy right and or similar rights closely related to copyright including without limitation perfor mance broadcast sound recording and Sui Generis Database Rights without regard to how the rights are labeled or categorized For purposes of this Public License the rights spec ified in Section 2 b 1 2 are not Copyright and Similar Rights Effective Technological Measures means those measures that in the absence of proper authority may not be circumvented under laws fulfilling obligations under Article 11 of the WIPO Copyright Treaty adopted on December 20 1996 and or similar international agree ments Exceptions and Limitations means fair use fair dealing and or any other exception or limitation to Copyright and Simila
13. by the Licensor to the extent possible the Licensor offers the Licensed Material as is and as available and makes no repre sentations or warranties of any kind con cerning the Licensed Material whether express implied statutory or other This includes without limitation warranties of title merchantability fitness for a partic ular purpose non infringement absence of latent or other defects accuracy or the presence or absence of errors whether or not known or discoverable Where dis claimers of warranties are not allowed in full or in part this disclaimer may not ap ply to You b To the extent possible in no event will the Licensor be liable to You on any legal the ory including without limitation negli gence or otherwise for any direct special indirect incidental consequential puni tive exemplary or other losses costs ex penses or damages arising out of this Pub lic License or use of the Licensed Mate rial even if the Licensor has been advised of the possibility of such losses costs ex penses or damages Where a limitation of liability is not allowed in full or in part this limitation may not apply to You c The disclaimer of warranties and limitation of liability provided above shall be interpreted in a manner that to the extent possible most closely approximates an absolute disclaimer and waiver of all liability Section 6 Term and Termination a This Public License appli
14. mands for opening and generating graph transformation systems configuring external programs and changing user preferences e In the rule selection box the user can se lect the rule of the currently opened graph transformation system which is displayed In the rule display the currently selected rule is displayed One can change the layout of the rule by dragging nodes and control points of edges When multiple nodes and edges are selected they can be moved simul taneously by dragging the selection box or rotated by dragging the quarter circle in the top left corner of the selection box Currently it is not possible to modify the structure of the rule In the action panel the user can select the ac tion she wants to perform prove compare or trace and give the algorithm or algorithms which are to be used in this action In the right of the action panel is the Execute but 2 THE GRAPHICAL USER INTERFACE AdHocRouting Grez System Options Help Select rule send message SSS Prove Compare Trace Algorithms TypeGraph smt Tool 23 Nodes 3 WT TA Edit Execute 3rules Signature R M U C S Figure 2 1 Main window of Grez ton which executes the currently selected Generate random GTS Generates action a random graph transformation sys tem with user specified parameters see e At the bottom is the status bar which dis 2 4 2 plays information about the currently op
15. when one of the algorithms returned a result but not when no termination or non termination proof could be found Always The log is always automati cally closed after all algorithms finished This causes Grez to finish silently when no proof can be found 2 9 Getting help Grez does not provide an online help system Its documentation consists of this user manual and the web site Under the Help menu you can find two menu items Visit website will open Grez s website in your standard browser and About dis plays version and license information of Grez Three The Command Line Interface Almost all functionality of Grez can also be ac cessed from the command line This is mainly useful if you want to start Grez from a shell script or another application for example to perform batch processing In this chapter we describe the command line interface of Grez One thing you cannot do with the command line interface is configuring external tools such as other termination provers and SMT solvers For this you need the graphical user interface see 2 7 After an external tool has been configured it is available through the command line interface however 3 1 Using Grez from the command line From the directory where the file grez jar is located Grez is started from the command line with following command java jar grez jar cli lt args gt When a suitable shell script is created in the path see
16. 1 is equivalent to the def initions n1 e A gt n2 and e A n1 n2 The latter two variants can be chained For example ni e A gt n2 B gt n2 lt A n3 defines three edges one A labelled edge from n1 to n2 one B labelled edge from n2 to n2 a loop and one A labelled edge from n3 to n2 a loop Only the first of these edges is given a name e All nodes occurring in edge definitions are also implicitly added to the graph If more nodes are to be added to the graph we can do so by the node keyword node n4 18 adds a node named n4 to the graph In practice the node keyword is only required to add nodes to the graph which are not incident to any edge that is isolated nodes The correspondence morphism of the rule is im plicitly defined to be the partial morphism which maps nodes and edges of the left hand side to the node or edge of the right hand side with the same name if it exists Example 4 1 1 Consider the following SGF code MyRule rule ni A gt n2 A gt n3 gt B n1 n4 n3 L E defines a rule which removes pairs of consecutive A labelled edges and replaces them by a single hyperedge labelled B The node n2 of the left hand side is removed and the node n4 of the right hand side is created when this rule is applied 4 1 2 Defining graph transformation systems A graph transformation system is defined as fol lows lt name gt gts rules lt
17. 8 License Still if you have feedback bug reports and questions you may send them to the main devel oper by e mail sanderbruggink gmail com Please indicate Grez in the subject line If time allows for it you might even get an answer 1 7 How to read this manual This manual is not intended to be read sequen tially In particular the theoretical foundations of the variant of graph transformation that Grez uses as well as of the algorithms that it employs to find termination proofs are covered in Chap ter 5 so if you want to know the theory behind Grez you should start there Grez offers to main user interfaces a graphi cal user interface and a command line interface which are covered in Chapters 2 and 3 respec tively If you are not interested in the graphical user interface you do not need to read Chapter 2 and if you do not want to use the command line interface you do not need to read Chapter 3 Chapter 4 presents the file format that Grez uses Since Grez currently lacks a graphical user interface for specifying graph transformation sys tems you need to read this chapter if you want to apply it to your own graph transformation systems 1 8 License Grez is distributed under the terms of the three clause BSD license see Appendix A 1 The two main third party libraries used are ANTLR and Google Guava The first is like Grez itself distributed under the terms of the three clause BSD license
18. Grez User Manual H J Sander Bruggink Contents Contents i 1 Introduction 1 1 1 Introduction to Grez 4 au 2 Eh ah Br e Re neh 1 1 2 Name Tin va ann Da a He ae sd o a a ee de 1 1 3 Peoples ara ey ty ran artes ae aha a ee gees ge ie an ee we ee 2 1 4 System requirements 2 Comm 2 1 5 Installation ya ess dial Pace a na ee 2 1 6 Feedback and bug reports o ee 2 1 7 How to read this manual o 3 1 8 license oe a GS A A da ee 3 2 The Graphical User Interface 5 2 1 Running Grez nn nn 5 2 2 The main window aoaaa a 5 2 3 The main menu 2 2 2 2 nn nn 6 2 4 Opening graph transformation systems 2 222 mon nn 7 2 4 1 Reading a system from a file oo nn 20 2 0 02000200 7 2 4 2 Generating random systems 22 22 Con nn nn 7 2 5 AGON y o See eee a ee we ee Meee aa da ha ee 8 2 5 1 Proving termination 0 0 000000 ee 8 2 5 2 Comparing algorithms 22 2 2 Common 9 2 5 3 Generating traces ooo 9 2 6 Specifying algorithms 2 2 0 00 20 0 a 9 2 6 1 The algorithm list editor 20 0000 00 ee ee 9 2 6 2 The algorithm editor 0 000000 eee 9 2 7 Configuring external tools 2 2 nn nn 10 2 7 1 Configuring SMT solvers 2 Co 1 10 2 7 2 Configuring termination tools 0000002 eee 11 2 8 Changing user preferences 2 2 2 12 2 9 Getting help 2 lt ars cn a ed eee e AR EERE SE we EE ee 12 3 The Command Line In
19. al tools called by it is only possible with the graphical user interface but other than that all Grez functionality can be accessed through both interfaces Grez is written in Java 8 and uses the standard Java libraries including Swing and concurrency JavaCC ANTLR and Google Guava as well as a number of in house libraries for graph trans formation and visualization For some optional functionality it needs an external tool in partic ular an SMT solver to find solutions for sets of constraints and a IATEX distribution to generate PDF reports 1 2 Name People have wondered where the name Grez comes from There are two slightly different things that people want to know when they ask this question Some people who ask this question are curious about what Grez means An implicit assump tion here is that every name must mean something Amsterdam is a city which grew around a dam built in the river Amstel England is the land of the angles an ancient Germanic tribe Columbia is named after Christopher Columbus But that is not the case here There is no language know of current or historic where the letter sequence G R E Z has any sensible meaning other than some word which starts with a G and ends with az Other people do not want to know what Grez means but what the reason is that the name Grez was picked for this particular piece of software This is an entirely different question one with an a
20. am value pairs If an algorithm has no pa rameters the parentheses are optional The value can be any string not containing a comma If the parameter requires an integer value value must be an non negative integer a sequence of digits and if the parameter is a boolean parameter value must be either true or false if the value is to be set to true true can be omitted The possible algorithms are list below Here an arbitrary string is denoted by s a non negative integer by n and a boolean value by b CycleFinder Tries to prove non termination by constructing a cycle This algorithm is described in 85 4 1 EdgeCounter Tries to prove termination by showing that the number of edges with a label from a certain set decreases in each rule application This algorithm is described in 85 4 3 External tool s Calls an external termina tion tool the name of which is given by the tool parameter External tools can only be configure using the graphical user interface see 2 7 2 MatchBound size n limit n mini b in b out b Tries to prove termination by using the match bound method described in 85 4 6 The size parameter specifies the size of the initial graph the limit parameter specifies after how many iterations the algorithm is aborted The parameters mini in and out turn on or off conservative minimization incoming factorization and outgoing factorization respectively NodeCounter
21. and side plus one 3 Reduce the type graph by user specified type graph reductions see below 4 Continue with step 2 as long as the type graph can be modified this way If the algorithm terminates then a type graph for the annotated graph transformation system has been found and thus the original graph transfor mation system is terminating Grez implements the following type graph re ductions e Conservative minimization While the type graph has an endomorphism a morphism from the type graph to itself which is not an isomorphism the type graph is replaced by the image of this endomorphism This reduction is conservative in the following sense Let T be a type graph and T its 5 4 Algorithms for proving termination and non termination minimization Then there exists a morphism f G T if and only if there exists a mor phism f G gt T Outgoing edge factorization If there are two edges with the same label which are connected to the same node in port 0 in binary edges this is the source port then the nodes connected to port 1 the target port of the two edges are merged This is a non conservative reduction Let T be a type graph and 7 its outgoing edge factorization Then it is the case that the existence of a morphism f G T implies the existence of a morphism f G gt T but not the other way around For some graph transformation systems this reduction is necessary for the algor
22. and side and a right hand side but also of the correspondence morphism So we do not want to compare the left hand side and the right hand side in isolation but also want to consider the correspondence morphism to get stronger termination arguments We will call a rule p decreasing resp non increasing if it holds that G H implies G gt H resp G gt H where gt is a well founded ordering on graphs which depends on the specific technique and gt is the reflexive closure of gt Now it holds that a graph transformation system is terminating if all its rules are decreasing A useful notion is that of relative termination Let R be a set of graph transformation rules that is R is a graph transformation system If R can be partitioned into two sets R and RT RAR such that all rules of R are decreasing and all rules of R are non increasing then R is termi nating if and only if R is terminating Often proving that R is terminating is considerably easier than proving that R is terminating Thus iterative termination proofs are produced Many termination techniques employed by Grez support 5 4 Algorithms for proving termination and non termination relative termination 5 3 Satisfiability modulo theories Some algorithms used by Grez solve constraints by translating them into a satisfiability modulo the ories SMT formula and then calling an external SMT solver Here we briefly describe SMT The SMT pro
23. ation proving they are mentioned here for the sake of completeness but can otherwise be ignored when specifying graph transformation systems for use with Grez They are not further mentioned in this chapter An identifier in SGF is any non empty sequence of letters a z and A Z digits 0 9 and the special symbols _ and which is not a keyword Identifiers and keywords in SGF are case sensitive that is myRule is not the same token as myrule or MYRULE Identifiers function both as names of defined objects nodes and edges and as labels of edges name identifier label identifier C C style comments can be used through out SGF code on encountering everything until the end of the line is ignored and addition ally every symbol between and x is ignored 4 2 2 Object definitions An SGF file consists of a list of object definitions sgf gt object Each object definition defines an object of a certain type For Grez only graphs graph morphisms morphism graph transformation rules rule and graph transformation systems gts are relevant Optionally each defined object is given a name by preceding the object definition with name where the name is an identifier By giving an object a name it is possible to refer to the object later Each object definition ends with a semicolon object gt
24. blem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first order logic with equality Examples of theories typically used in computer science are the the ory of real numbers the theory of integers and the theories of various data structures such as lists arrays bit vectors and so on SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming Formally speaking an SMT instance is a for mula in first order logic where some function and predicate symbols have additional interpre tations and SMT is the problem of determining whether such a formula is satisfiable In other words imagine an instance of the Boolean satisfi ability problem SAT in which some of the binary variables are replaced by predicates over a suitable set of non binary variables A predicate is basi cally a binary valued function of non binary vari ables Example predicates include linear inequali ties for example 3x 2y z gt 4 or equalities involving uninterpreted terms and function sym bols for example f f u v v f u v where f is some unspecified function of two unspecified arguments These predicates are classified ac cording to the theory they belong to For instance linear inequalities over real variables are evaluated using the rules of the theory of linear real arith metic whereas predicates i
25. custom graph transforma tion system he must use an external program to create a file which describes the wanted graph transformation system The file format that Grez natively supports called the simple graph format SGF is a text based format that describes various objects which play a role in graph transformation such as graphs and hypergraphs morphisms and rules The format was developed to have a single parser and input format that can be used in different graph transformation tools Unlike other text based formats such as XML derived formats which are mainly designed to be easily parsed by a computer program SGF is designed to be easily written read and maintained in source form by a human being the word simple in the name reflects that it is supposedly simple to write not that it describes simple graphs One of the results of the emphasis on easy writing rather than easy parsing is that there is sometimes more than one way to define the same object In this chapter we describe the fragment of SGF which describes objects that Grez understands namely graphs rules morphisms and graph trans formation systems 4 1 A first tour An SGF file consists of a list of object definitions Each of the objects defined in an SGF file can either be nameless or be named by an identifier If it is named by an identifier object definitions occurring later in the file may refer to the object by using its name The types of ob
26. en called from Grez If the command line argu ments contain the literal string FILE or F ILE this string is replaced by the input file name If it is required to pass an input file name to the tool but none of the two string is present then Grez adds the input file name to the end of the command line e Input method Whether the SMT solver expects its input to be passed through the standard input stream or via a temporary file on disk Grez expects SMT solvers to write their output in SMT LIB 2 format to the standard output stream In principle Grez support any SMT solver which can read files in SMT LIB 2 format and produces results and models in the same format Some SMT solvers which claim to be compatible with SMT LIB 2 however are not or not completely Grez was tested and found to work with CVC4 1 and Z3 2 Other solvers might also work it is up to the user to try out 2 7 2 Configuring termination tools To configure external termination tools used by Grez select the Termination tools item from the Options menu A dialog appears with which you can add remove and edit the configurations for the external termination tools For each termina tion tool the following information is required e Name The name of the tool This name is used to refer to the tool in user interactions e Executable Full path of the executable file of the tool Click the Browse button to select the executable in a fi
27. en graph transformation system in particular the number of rules and the edge labels oc curring in it Exit Quit Grez e Options Command for configuring Grez Termination tools Configure external termination tools used by Grez see 2 3 The main menu y 2 7 2 Grez s main menu contains the following menus SMT solvers Configure SMT solvers and commands used by Grez see 2 7 1 GUI options Change some preferences A made glenn for the graphical user interface see transformation systems 82 8 Open GTS Open a system from a file Change number of worker threads see 82 4 1 Change the number of worker threads 2 4 Opening graph transformation systems that Grez uses when proving or com paring algorithms the default is the number of separate CPU cores in the computer e Help Obtain information about the pro gram see 2 9 Visit website Open Grez s website in a browser window About Display copyright license and version information of Grez 2 4 Opening graph transformation systems There are two ways to open a graph transfor mation system reading a graph transformation system from a file or generating a random one 2 4 1 Reading a system from a file A graph transformation system can be read from a file in two ways on the command line and through the graphical user interface e On the command line Specify the file con taining t
28. entity including a cross claim or counterclaim in a law suit alleging that the Work or a Contribution incorporated within the Work constitutes direct or contributory patent infringement then any patent licenses granted to You under this License for that Work shall terminate as of the date such litigation is filed 4 Redistribution You may reproduce and dis tribute copies of the Work or Derivative Works thereof in any medium with or without modifi cations and in Source or Object form provided that You meet the following conditions a You must give any other recipients of the Work or Derivative Works a copy of this License and A 2 Apache License version 2 0 b You must cause any modified files to carry prominent notices stating that You changed the files and c You must retain in the Source form of any Derivative Works that You distribute all copy right patent trademark and attribution no tices from the Source form of the Work ex cluding those notices that do not pertain to any part of the Derivative Works and d If the Work includes a NOTICE text file as part of its distribution then any Derivative Works that You distribute must include a read able copy of the attribution notices contained within such NOTICE file excluding those no tices that do not pertain to any part of the Derivative Works in at least one of the fol lowing places within a NOTICE text file dis tributed as part of the Deri
29. er hand each edge can only be defined once Defining two edges with the same name will result in an error even if they have the same label in both cases 4 2 4 Morphisms Morphisms are defined by the keyword morphism as follows 4 2 Grammar morphism morphism from name to name mappings mappings mapping mapping mapping name gt name Every morphism has a domain graph given af ter the from keyword and a codomain graph given after the to keyword In some cases for example when defining a rule the domain and codomain can be determined from the context in these cases explicitly specifying the domain and the codomain is optional In all other cases the domain and codomain must be specified The body of a morphism definition consists of a semicolon separated list of individual mappings which map nodes of the domain graph to nodes of the codomain and edges of the domain to edges of the codomain When mapping an edge it is not necessary to explicitly map the incident nodes of that edge also this is done automatically If the specified mapping does not represent a partial morphism in particular this happens when a node or an edge of the domain is mapped to two different nodes or edges of the codomain an error is reported 4 2 5 Transformation rules A transformation rule consists of a left hand side a right hand side and a correspondence morphism
30. es all subsets of the graph transformation system s signature and returns a termination proof if the above condition holds for one of those subsets 5 4 4 Petri net approximation In 9 a termination technique was presented which over approximates the transition sequences of a graph transformation system by a Petri net If the Petri net is terminating which is the case if a certain system of linear inequalities does not 28 have any trivial solutions then the graph transfor mation system is terminating as well In fact the paper 9 extends this result to graph transforma tion systems with negative application conditions of a certain kind but since Grez does not sup port negative application conditions at this point this extension was not implemented The Petri net that approximates the graph transformation system has a place for each label in the signature and a transition for each graph transformation rule The pre and post conditions of the Petri net are as follows for each edge la belled with a label A in the left hand side of a rule p the place corresponding to A is added as a pre condition to the transition corresponding to p and for each edge labelled with a label B in the right hand side of a rule p the place cor responding to B is added as a post condition to the transition corresponding to p Note that the Petri net only models the number of edges with a certain label it does not model the structure of the gra
31. es confuse the graph G with the set of its components G Va U Eg In this chapter we will additionally assume without loss of generality that for two graphs G and H Va and Ey are disjoint in other words we assume global disjoint universes of nodes and edges The graph labels come from a fixed set A called the signature In Grez the signature consists of all identifiers that is strings consisting of letters digits and some special characters see 4 2 1 can function as labels The subset of labels that occur in a graph G is called the signature of G If G is a graph e is an edge of G and v a node of G then we will say that e and v are incident if v attg e Furthermore two edges es and are adjacent if there exists a node v which is incident to both e and eg Similarly two nodes v and uz are called adjacent if there exists an edge which is incident to both v and us A morphism f from a graph G to a graph H is a function which maps nodes of G to nodes of H and edges of G to edges of H such that for each edge e Eg laba e laby f e and f attg e atty f e Grez employs the so called double pushout ap proach to graph transformation 6 However for performance and convenience reasons graph transformation rules are represented similar to single pushout rules A graph transformation rule consists of two graphs a left hand side L and a right hand side R and a partial injective mor p
32. es for the term of the Copyright and Similar Rights licensed here However if You fail to comply with this Public License then Your rights under this Public License terminate automatically Where Your right to use the Licensed Ma terial has terminated under Section 6 a it reinstates 1 automatically as of the date the violation is cured provided it is cured within 30 days of Your discovery of the violation or 2 upon express reinstatement by the Licensor For the avoidance of doubt this Section 6 b does not affect any right the Licensor may have to seek remedies for Your violations of this Public License For the avoidance of doubt the Licensor may also offer the Licensed Material under separate terms or conditions or stop distributing the Licensed Material at any time however doing so will not terminate this Public License Sections 1 5 6 7 and 8 survive termination of this Public License Section 7 Other Terms and Conditions a The Licensor shall not be bound by any addi tional or different terms or conditions commu nicated by You unless expressly agreed Any arrangements understandings or agree ments regarding the Licensed Material not stated herein are separate from and indepen dent of the terms and conditions of this Public License 39 A LICENSE TEXTS Section 8 Interpretation a 40 For the avoidance of doubt this Public License does not and shal
33. giving a string rep resentation of the distribution The followings distributions are available for all options where a distribution is required e Non random A single number which is al ways chosen The syntax is simply this num ber for example 3 or 0 25 e Uniform All numbers within a speci fied range have an equal probability The string representation of such a distribution is uniform min max e Normal Normal distribution with a given mean and standard deviation The string representation of such a distribution is normal mean sd where sd is the stan dard deviation 2 5 Actions Grez has three main actions to perform on graph transformation systems it can try to automat ically prove that a given graph transformation system terminates or not using a number of al gorithms 82 5 1 it can compare the result of a number of algorithms 2 5 2 and it can produce a trace for a single algorithm 2 5 3 2 5 1 Proving termination To prove termination of a graph transformation system choose the Prove tab from the action panel give the algorithms which are to be used for proving termination and press the Execute button When proving termination Grez runs a number of user selected algorithms concurrently As soon as one algorithm returns a proof of termination or non termination of the graph transformation system under consideration all algorithms are stopped and the found proof is reported to the u
34. hat are managed by or on behalf of the Licen sor for the purpose of discussing and improving the Work but excluding communication that is conspicuously marked or otherwise designated in writing by the copyright owner as Not a Contri bution Contributor shall mean Licensor and any in dividual or Legal Entity on behalf of whom a 34 Contribution has been received by Licensor and subsequently incorporated within the Work 2 Grant of Copyright License Subject to the terms and conditions of this License each Contributor hereby grants to You a perpetual worldwide non exclusive no charge royalty free irrevocable copyright license to reproduce prepare Derivative Works of publicly display publicly per form sublicense and distribute the Work and such Derivative Works in Source or Object form 3 Grant of Patent License Subject to the terms and conditions of this License each Contrib utor hereby grants to You a perpetual worldwide non exclusive no charge royalty free irrevocable except as stated in this section patent license to make have made use offer to sell sell im port and otherwise transfer the Work where such license applies only to those patent claims licensable by such Contributor that are necessarily infringed by their Contribution s alone or by com bination of their Contribution s with the Work to which such Contribution s was submitted If You institute patent litigation against any
35. he GTS on the command line If this file contains more than one GTS the name of the GTS must be specified using the system name command line option See Chapter 3 for more information e Through the graphical user interface Select Open GTS from the System menu A file dialog appears Select the file containing the graph transformation system you want to open When selecting a file in the right of the dialog a list of graph transformation systems in this file appears Select the one you want to open and click Open 2 4 2 Generating random systems Grez provides the option of automatically gener ating GTSs To generate a random graph trans formation system select the Generate random GTS menu item from the System menu A dialog appears in which the parameters of graph trans formation system generation can be specified The parameters can be divided in four parts general parameters parameters for the left hand side parameters for the right hand side and pa rameters for the interface of the rule General parameters e Number of rules This is a single number which specifies the number of rules in the randomly generated GTS Signature The labels that can occur in the GTS and their arities This is a comma separated list of entries of the form Label arity where label is the string displayed on the edge and arity is the arity of the label that is the number of nodes edges labeled with this label are incident to Al
36. he currently selected algorithm from the list e Clear Removes all algorithms from the list e Edit Opens the Algorithm editor to edit the currently selected algorithm e Move up Moves the currently selected al gorithm one position up in the list e Move down Moves the currently selected algorithm one position down in the list Default Replaces the list by the default list of algorithms Complete Adds to the algorithm list all algorithms of the default list for which there is not already an algorithm of the same type but possibly with different parameters in the list 2 6 2 The algorithm editor In the algorithm editor we can specify the algo rithm type and for each type we can give a number of parameters The following algorithm types are available e Cycle finder Tries to prove non termination of the selected graph transformation system by trying to construct a cycle This algorithm is described in 5 4 1 The parameters are 9 2 THE GRAPHICAL USER INTERFACE 10 Initial graph size number of nodes in the initial graph Length limit length of the transfor mation sequences which are generated e Node counter Tries to prove termination by showing that the number of nodes decreases in each rule application This algorithm is described in 5 4 2 e Edge counter Tries to prove termination by showing that the number of edges with a label from a certain
37. here each node and edge has been given a weight N Rules can be evaluated with respect to a weighted type graph in two ways tropically and arcticly see below In each of these cases a graph transformation system is proved to be ter minating by finding a weighted type graph which satisfies the properties required by the chosen evaluation type Grez s type graph algorithm sup ports two methods for find tropically arcticly or arithmetically evaluated weighted type graphs the first is a naive implementation which exhaus tively enumerates all weighted type graphs up to a certain number of nodes and maximum weight the second encodes the properties as an SMT for mula and runs an external SMT solver to find a weighted type graph with k nodes satisfying these properties where k is a user specified parameter Tropical evaluation This termination tech nique was introduced in 5 The technique sup ports relative termination Given a weighted type graph T the weight of a morphism m G T denoted wt m is the sum of all the weights in its image Then a rule p L gt R with correspondence morphism f is called tropically decreasing with respect to T if for each morphism mz L T there exists a morphism mp R T which agrees on f such that wt m gt wt mp it is called tropically non increasing with respect to T if for each morphism mz L T there exists a mor phism mp R T which agrees on f such that wt mz
38. hism from L to R The morphism f will be called the correspondence morphism Without loss of generality it will always be assumed that the correspondence morphism f is of the following T In this case f is extended to sequences of nodes as follows f v1 Un f v f Un 25 5 THEORETICAL FOUNDATIONS form x fzeLnR undefined otherwise f x Using this assumption the equivalent rule in the normal double pushout style is obtained by taking LN R as the interface and the two injections as the rule span A graph transformation step can be algorithmi cally described as follows Let a rule p L gt R with correspondence morphism f be given Sup pose there exists an injective morphism m the match from L into some graph G The rule can be applied to m if for every edge e Eg not in the image of m and node v attg e it holds that if v is in the image of m f is defined on the pre image of v under m In this case we say that the dangling edge condition is satisfied If the rule is applicable all images of elements in L for which f is undefined are removed from G This gives us the context graph C Furthermore the elements of R that do not have a preimage in L are added and connected with the remaining elements as specified f This results in the graph H and we write G H The dangling edge condition ensures that nodes can only be deleted if all incident edges are deleted Finally a graph transformati
39. ibility of such damages 35 A LICENSE TEXTS 9 Accepting Warranty or Additional Liability While redistributing the Work or Derivative Works thereof You may choose to offer and charge a fee for acceptance of support warranty indemnity or other liability obligations and or rights consistent with this License However in accepting such obligations You may act only on Your own behalf and on Your sole responsibility not on behalf of any other Contributor and only if You agree to indemnify defend and hold each Contributor harmless for any liability incurred by or claims asserted against such Contributor by reason of your accepting any such warranty or additional liability A 3 Creative Commons Attribution 4 0 International Public License By exercising the Licensed Rights defined below You accept and agree to be bound by the terms and conditions of this Creative Commons Attri bution 4 0 International Public License Public License To the extent this Public License may be interpreted as a contract You are granted the Licensed Rights in consideration of Your ac ceptance of these terms and conditions and the Licensor grants You such rights in consideration of benefits the Licensor receives from making the Licensed Material available under these terms and conditions Section 1 Definitions a Adapted Material means material subject to Copyright and Similar Rights that is derived from or based upon the
40. ination analysis of graph transformation systems In Proceedings of TCS 2014 volume 8705 of LNCS Springer 2014 Andrea Corradini Ugo Montanari Francesca Rossi Hartmut Ehrig Reiko Heckel and Michael Lowe Algebraic approaches to graph transformation Basic concepts and double pushout approach In Grzegorz Rozenberg editor Handbook of Graph Grammars and Computing by Graph Transformation vol 1 Foundations World Scientific 1997 Detlef Plump Termination of graph rewriting is undecidable Fundementa Informaticae 33 2 201 209 1998 Terese Term Rewriting Systems volume 55 of Cambridge Tracts in Theoretical Computer Science Cambridge University Press 2003 D niel Varr Szilvia Varr Gyapay Hartmut Ehrig Ulrike Prange and Gabriele Taentzer Termination analysis of model transformations by petri nets In Proceedings of ICGT 2006 volume 4178 of LNCS Springer 2006 Wikipedia Satisfiability modulo theories http en wikipedia org w index php title Satisfiability_Modulo_Theories amp oldid 635242269 2014 41 Index About menu item 7 12 action panel 5 actions 8 9 Add button 9 adjacent 25 Algorithm editor dialog 9 10 Algorithm list editor dialog 9 annotation 20 arctic evaluation 29 Change number of worker threads menu item L Clear button 9 command line interface 13 15 command line options 13 14 action 14 algos 14 beta 5 14 c 13 cli 13 conn 14 dens 14
41. ithm to terminate while in others it causes non termination Incoming edge factorization The same as outgoing edge factorization but now nodes are merged if they are the source nodes of two edges with the same label and the same target node 31 Appendix A License texts A 1 BSD License Redistribution and use in source and binary forms with or without modification are permitted pro vided that the following conditions are met 1 Redistributions of source code must retain the above copyright notice this list of condi tions and the following disclaimer 2 Redistributions in binary form must repro duce the above copyright notice this list of conditions and the following disclaimer in the documentation and or other materials provided with the distribution 3 Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission This software is provided by the copyright holders and contributors as is and any express or implied warranties including but not limited to the im plied warranties of merchantability and fitness for a particular purpose are disclaimed In no event shall the copyright holder or contributors be liable for any direct indirect incidental special exem plary or consequential damages including but not limited to procurement of substitute goods or services
42. ject that are mainly important for Grez are graph transformation rules rules for short and graph transformation systems which are sets of rules In this section the most common way to define such objects is presented For a complete reference on how these objects can be defined the reader is referred to 4 2 4 1 1 Defining rules Rules are defined in the following way lt name gt rule lt left hand side gt gt 17 4 SPECIFYING GRAPH TRANSFORMATION SYSTEMS THE SIMPLE GRAPH FORMAT lt right hand side gt hs The lt name gt part is optional if you want to define a rule with a default name The left hand side and right hand side are blocks delimited with L and defining the nodes and edges of the respective graph the node and edge definitions are separated by semicolons An edge can be defined in the following ways e e A ni nk denotes a hyper edge with name e and label A which is incident to the nodes n1 nk Giving a name to an edge is optional if it is absent the edge will not be in the correspondence morphism of the rule e ni e A gt n2 denotes a binary edge with source node n1 and target node n2 Again the name of the edge is optional The defi nition n1 e A gt n2 is equivalent to the definition e A n1 n2 e n2 lt e A n1 denotes a binary edge with source node n1 and target node n2 Again the name of the edge is optional The defini tionn2 lt e A n
43. l not be interpreted to re duce limit restrict or impose conditions on any use of the Licensed Material that could lawfully be made without permission under this Public License To the extent possible if any provision of this Public License is deemed unenforceable it shall be automatically reformed to the minimum ex tent necessary to make it enforceable If the provision cannot be reformed it shall be sev ered from this Public License without affecting the enforceability of the remaining terms and conditions No term or condition of this Public License will be waived and no failure to comply consented to unless expressly agreed to by the Licensor Nothing in this Public License constitutes or may be interpreted as a limitation upon or waiver of any privileges and immunities that apply to the Licensor or You including from the legal processes of any jurisdiction or au thority Bibliography 1 2 3 4 5 6 7 8 9 10 Cvc4 http cvc4 cs nyu edu web Z3 http z3 codeplex com H J Sander Bruggink Towards a systematic method for proving termination of graph transfor mation systems In Proceedings of GT VC 2007 2007 H J Sander Bruggink Barbara K nig Dennis Nolte and Hans Zantema Proving termination of graph transformation systems using weighted type graphs over semirings Submitted for ICGT 2015 2015 H J Sander Bruggink Barbara K nig and Hans Zantema Term
44. le dialog box Command line arguments The command line arguments to be passed to the tool when called from Grez If the command line argu ments contain the literal string FILE or FILE this string is replaced by the input file name If it is required to pass an input file name to the tool but none of the two string is present then Grez adds the input file name to the end of the command line Input format The file format in which Grez will translate the graph transformation sys tem prior to passing it to the tool The possible values are Simple graph format Pass the graph transformation system in simple graph format to the external tool String rewrite system Builds a cy cle rewrite system which is equivalent to the graph transformation system in terms of termination and then calls the tool on that Input method Whether the termination tool expects its input to be passed through the standard input stream or via a temporary file on disk Terminating regex If the tool s output matches this regular expression Grez will interpret this to mean the system is termi nating Non terminating regex If the tool s output matches this regular expression Grez will interpret this to mean the system is not terminating 11 2 THE GRAPHICAL USER INTERFACE 2 8 Changing user preferences By choosing GUI options from the Options menu the user can change the way Grez display
45. list of rules gt l F The list of rules is a comma separated list or rules Usually the list entries are names of rules defined earlier but it is also possible to define rules in place using the rule syntax of the previous section Example 4 1 2 A graph transformation system which only contains the rule of Example 4 1 1 is defined by the following SGF code 4 2 Grammar MyGTS gts rules MyRule 4 2 Grammar In this section we specify the grammar of the fragment of SGF which describes graph transfor mation systems and the objects on which they depend In the grammar fragments we use the follow ing conventions Terminal symbols are given in typewriter font and enclosed in double quotes for example graph and Non terminal sym bol are displayed in a slanted font We use a kind of extended Backus Naur form the right hand sides of the rules are basically regular expression consisting of optional parts choice and repetition 4 2 1 Tokens SGF tokens are delimited by whitespace space tab carriage return and line feed characters Oth erwise whitespace is ignored this means in par ticular that newlines are ignored and do not carry any meaning The following tokens are keywords in SGF copy ifgraph x rule from morphism system x graph node to gts not x trace x The keywords marked with a star are used to describe objects which are not used in the context of termin
46. ller graph transformation system 2 5 3 Generating traces Some algorithms can generate a trace to make visible in what order certain operations are tried out To generate a trace of an algorithm se lect the Trace tab of the action panel enter the algorithm to generate a trace of and click the Execute button The selected algorithm is exe cuted the steps of the algorithm are stored and after the algorithm finishes its trace and its result are reported to the user Note that generating a trace is not supported by all algorithms 2 6 Specifying algorithms There are two ways to specify the algorithms which are going to be run the string represen tation of the algorithm or algorithm list can be edited directly or it can be edited through a di alog If you want to edit the string directly see 83 3 for the syntax If you want to use the di alog press the Edit button to the right of the text box If the currently selected action is Prove or Compare the Algorithm list editor appears to specify the list of algorithms if the Trace action is selected the Algorithm editor appears to specify the algorithm 2 6 1 The algorithm list editor The algorithm list editor displays the list of repre sentations of algorithm on the left and a number of command buttons on the right Available com mand buttons are e Add Opens the Algorithm editor and adds the algorithm specified there to the algorithm list Remove Removes t
47. much more convenient in most circumstances In both cases edges have a label and optionally a name in the grammar called an edge annotation lNote however that an actual copy is made of the object thus the object will be represented in memory twice 20 edge_annot name label In the functional style edges are defined by definitions of the form A n Nnz where A is the annotation label and optionally the name of the edge and n1 ng are the names of the nodes incident to the edge edge edge_annot inc_nodes inc_nodes name name In the arrow style binary edges are defined by entries of the form src A gt tgt and tgt lt A src which denote binary edges from node sre to node tgt These entries can be chained for example x A gt y lt B z binedge name direction name direction gt edge_annot gt lt edge annot For both the functional style and the arrow style it holds that if one of the node names does not yet occur in the graph a node of that name is added to the graph Names Within a single graph each name can occur only once That is for each name there can be at most on node or edge with that name If a node name occurs in a graph definition multiple times then it refers to the same node in all cases In particular the edge definition x A gt x de fines an A labeled loop on the node named x On the oth
48. n to an external tool possibly after per forming some translation 2 7 Configuring external tools Two types of external tools can be used with Grez external SMT solvers and external termination tools The external SMT solvers are used by some algorithms to solve constraints while external termination tools serve as a kind of oracle Grez instructs them to prove termination of a graph transformation system after translating it to a format suitable for the tool and trusts that the result is correct External SMT solvers and termination tools need to be configured before Grez can use them In particular Grez needs to know where their ex ecutable files are what command line arguments the tools require how and in what format they expect their input and how to interpret their output 2 7 1 Configuring SMT solvers To configure the external SMT solvers used by Grez select the SMT solvers item from the Op tions menu A dialog appears with which you can add remove and edit the configurations for the external SMT solvers For each SMT solver the following information is required 2 7 Configuring external tools e Name The name of the SMT tool This name is used to refer to the tool in user interactions e Executable Full path of the executable file of the tool Click the Browse button to select the executable in a file dialog box e Command line arguments The command line arguments to be passed to the tool wh
49. name graph morphism rule gts copy To make a copy of a previously defined object we can use the copy keyword copy gt copy ieh name nyu 19 4 SPECIFYING GRAPH TRANSFORMATION SYSTEMS THE SIMPLE GRAPH FORMAT A declaration of the form copy name makes a copy of the object with the given name This is especially useful if you wish to store the same object under two names 4 2 3 Graphs Graphs are defined with the keyword graph followed by a description of the nodes and edges of the graph graph gt graph graph_desc The description of the nodes and edges of the graph is block delimited with curly braces contain ing a semicolon separated list of node and edge definitions graph_desc gt node_edge node edge node_edge node edge binedge Defining nodes Nodes can be defined by the node keyword followed by the name of the node Nodes have no label see Chapter 5 node node name A definition of the form node name makes sure that the graph contains a node with the given name if the graph already contains a node with that name a second node with the same name will not be added Defining edges Edges can be defined in two ways in a functional style which allows edges of arbitrary arity to be defined both binary edges and hyperedges and in an arrow style which only allows binary edges to be defined but which is
50. nsed Material automatically receives an of fer from the Licensor to exercise the Licensed Rights under the terms and conditions of this Public License B No downstream restrictions You may not offer or impose any additional or dif ferent terms or conditions on or apply any Effective Technological Measures to the Licensed Material if doing so re stricts exercise of the Licensed Rights by any recipient of the Licensed Material 6 No endorsement Nothing in this Public License constitutes or may be construed as permission to assert or imply that You are or that Your use of the Licensed Material is connected with or sponsored endorsed or granted official status by the Licensor or others designated to receive attribution as provided in Section 3 a 1 A i b Other rights 37 A LICENSE TEXTS 1 Moral rights such as the right of integrity are not licensed under this Public License nor are publicity privacy and or other simi lar personality rights however to the extent possible the Licensor waives and or agrees not to assert any such rights held by the Licensor to the limited extent necessary to allow You to exercise the Licensed Rights but not otherwise Patent and trademark rights are not li censed under this Public License To the extent possible the Licensor waives any right to collect royalties from You for the exercise of the Licensed Rights whether directly or through a collecting
51. nswer took the letters T E R and M which 1 INTRODUCTION are the first four letter of the word termination and the applied the well known ROT 13 cipher to them The result is Grez which coinciden tally starts with the same two letters as the word Graph 1 3 People The following people in alphabetical order are or were involved in the development of Grez either by directly implementing the tool or by providing its theoretical foundation e H J Sander Bruggink main developer e Barbara K nig e Dennis Nolte e Hans Zantema 1 4 System requirements Grez is written in Java To use Grez you need a recent Java virtual machine Java 8 or newer Additionally to export proofs to PDF you need a IATEX distribution installed including common packages and style files the command pdflatex must be in the path The performance of some algorithms is greatly improved if an external SMT solver is used SMT means satisfiability modulo theories and some algorithms even require this All SMT solvers which understand the SMT LIB 2 input format are supported External SMT solvers can be set up using the GUI and after that they are also available for use with the command line interface The standard Grez distribution contains all li braries that Grez uses thus other than Java itself you don t have to install additional software to run Grez To compile from source however you need the following e
52. nvolving uninterpreted terms and function symbols are evaluated using This section is adapted from Wikipedia 10 the rules of the theory of uninterpreted functions with equality sometimes referred to as the empty theory Other theories include the theories of arrays and list structures useful for modeling and verifying software programs and the theory of bit vectors useful in modeling and verifying hard ware designs Most SMT solvers support only quantifier free fragments of their logics Grez employs only the theories of linear integer arithmetic beta algorithms also non linear integer arithmetic and uninterpreted functions using quantifier free logic 5 4 Algorithms for proving termination and non termination 5 4 1 Finding cycles Grez implements a simple cycle finder which ex haustively generates all transition sequences up to a given length which start with an arbitrary initial graph with a given size If a cycle exists among these finitely many transition sequences this constitutes a proof of non termination 5 4 2 Node counting The node counting technique is a simple termina tion technique which supports relative termination Let G denote the number of nodes of a graph G This induces a well founded order on graph by counting the number of nodes A rule p L gt R is node decreasing if L gt R and it is non node increasing if L gt R Clearly when G H G gt H if p is n
53. o open an SGF file which con tains two graph transformation systems she must specify the name of the system she wants to open either by using the system lt name gt command line option or selecting it in the open dialog of the graphical user interface 4 3 2 in place definition In almost all cases where you can use the name of a previously defined object you can also define that object in place The exception to this rule is in the definition of a morphism after the from and to keywords you can only use the name of a previously defined graph For example MakeTriangle gts rules rule T 1 2 3 T gt 1 A gt 2 A gt 3 A gt 1 l If you define an object in place you cannot give it a name and thus you cannot refer to it later Defining an object in place can be advantageous if you need an object only once and do not want to introduce a new name 4 3 Examples 4 3 3 Ad hoc routing The following example is adapted from 5 The example describes a simple ad hoc routing proto col in a dynamically changing network A message M traverses a network of servers S routers R and directed connections C between them The message can only be sent to unvisited U nodes In addition rules which modify the net work s layout are active The graph transforma tion system which models the protocol consists of the following rules 9 e C 1 2 Send VN gt aia REY LADY
54. ode counting 27 5 4 3 Edge counting nun nn 28 5 4 4 Petri net approximation Hmm nn 28 5 4 5 Type graph techniques 2 22 22 m nn nn 29 5 4 6 Match bounds 30 A License texts 33 Al SBSDikieense s os Bes ee ee ee Oe ee Bel Da ee 33 A 2 Apache License version 2 0 2 2 2 2 on nn 33 A 3 Creative Commons Attribution 4 0 International Public License 36 Bibliography 41 Index 43 One Introduction 1 1 Introduction to Grez Termination the absence of infinite computations is a property that is required in many applications in particular in model transformation algorithms and protocol specifications Many of these appli cations such as graphical model transformation for example of UML models and algorithms that manipulate data structures on the heap are naturally modeled by graph transformation sys tems Grez is a software tool that given a graph transformation system automatically tries to find a proof that the graph transformation system terminates or a proof that it does not It does this by running a number of algorithms concur rently and reporting the result of the first of them that successfully finishes Since the problem is undecidable in general 7 in many cases none of the algorithms will find a termination or non termination proof Grez provides both a graphical user interface and a command line interface Configuring Grez in particular the paths and parameters of the extern
55. ode decreasing and G gt H if p is non node increasing This leads to the following termination argument Theorem 5 4 1 If R and S are graph trans formation systems such that all rules of R are node decreasing and all rules of S are non node 27 5 THEORETICAL FOUNDATIONS increasing then RUS is terminating if and only if S is The node counter algorithm used by Grez uses this termination argument It just checks if the condition applies and returns a termination proof if it does 5 4 3 Edge counting The edge counting technique is a simple termina tion technique which supports relative termination Let S C A be a set of labels then for a graph G s G denotes the number of edges in G which are labelled with a label from S A rule p L gt R is edge decreasing with re spect to S if 5 L gt s R and it is non edge increasing with respect to S if 9 L gt s R Clearly when G gt H 5 G gt s H if p is edge decreasing with respect to S and s G gt s H if p is non edge increasing with respect to S This leads to the following termina tion argument Theorem 5 4 2 Let S C A be a set of labels If R and S are graph transformation systems such that all rules of R are edge decreasing with respect to S and all rules of S are non edge increasing with respect to S then RUS is ter minating if and only if S is The edge counter algorithm used by Grez uses this termination argument It tri
56. on system is a fi nite set of graph transformation rules The rewrite relation induced by the graph transformation sys tem is the union of the rewrite relations induced by its rules 5 2 Termination There are two kinds of termination uniform and non uniform termination A graph transforma tion system is uniformly terminating if it does not allow an infinite transformation sequence Go gt G gt where Go is an arbitrary graph A graph transformation system is non uniformly terminating with respect to a set of graphs if 26 it does not allow an infinite transformation se quence Go gt Gi gt with Go L Grez only proves uniform termination although in future versions also non uniform termination might be supported A lot of research has been done on techniques for proving uniform termination of rewrite sys tems in particular of term and string rewrite systems An overview of such techniques can be found in 8 Chap 6 In general termination of a term or string rewrite system is proven by finding a suitable well founded ordering gt on the terms or strings In particular it is convenient if the ordering has the following property if L gt r for some rule p L gt r and s gt t then s gt L Now if we want to show that a term or string rewrite system is terminating it suffices to check that gt r for each rule of the system In graph transformation the rules do only con sist of a left h
57. on the meaning of these op tions and the syntax for specifying distributions see 82 4 2 left size dist Set the distribution for the number of nodes in the left hand side right size dist Set the distribution for the number of nodes in the right hand side if size dist Set the number of nodes in the interface left dens dist Set the distribution for the density of the left hand side right dens dist Set the distribution for the density of the right hand side dens dist Set the distribution for the den sity of the left hand side and right hand side at the same time left conn conn Set the connectedness of the left hand side possibilities are all connected and noiso right conn conn Set the connectedness of the right hand side possibilities are all connected and noiso conn conn Set connectedness of the left hand side and right hand side at the same time discrete bool Set whether or not the in terface is discrete default value true rules num Set the number of rules to gen erate 3 3 Specifying algorithms labels list Set the signature of the gen erated graph transformation system The value List is a comma separated list of entries of the form label arity 3 3 Specifying algorithms The general syntax for specifying algorithms is the following Algorithm Parameters where Parameters is a comma separated list of par
58. ormation or translation of a Source form including but not limited to compiled object code generated documentation and conversions to other media types Work shall mean the work of authorship whether in Source or Object form made available under the License as indicated by a copyright notice that is included in or attached to the work Derivative Works shall mean any work whether in Source or Object form that is based on or derived from the Work and for which the editorial revisions annotations elaborations or other modifications represent as a whole an orig inal work of authorship For the purpose of this License Derivative Works shall not include works that remain separable from or merely link or bind by name to the interfaces of the Work and Derivative Works thereof Contribution shall mean any work of author ship including the original version of the Work and any modifications or additions to that Work or Derivative Works thereof that is intentionally submitted to Licensor for inclusion in the Work by the copyright owner or by an individual or Legal Entity authorized to submit on behalf of the copy right owner For the purposes of this definition submitted means any form of electronic verbal or written communication sent to the Licensor or its representatives including but not limited to communication on electronic mailing lists source code control systems and issue tracking systems t
59. ph Clearly each transformation sequence of the graph transformation system induces a firing se quence of the Petri net of the same length Thus termination of the Petri net implies termination of the graph transformation system but not vice versa A non termination Petri net is called weakly repetitive in the Petri net literature To check whether a Petri net is weakly repetitive the fol lowing well known result can be used Proposition 5 4 3 Let A be the incidence ma trix of a Petri net M Then M is weakly repetitive if there exists a vector z with z gt 0 and z 0 such that AT x z gt 0 Grez s Petri net approximation algorithm uses an external SMT solver to check whether the inequality of the above proposition has any so lutions since it is a linear inequality this is a decidable problem 5 4 Algorithms for proving termination and non termination 5 4 5 Type graph techniques A type graph for a graph transformation system R is a graph T such that for each reachable graph G there exists a morphism from G to T Since Grez only supports uniform termination effectively this means that for each graph G there exists a morphism from G to T We additionally require that for each rule p R where p L gt R and p has correspondence morphism f and morphism m L gt T there exists a morphism m R gt T such that m o f x m x for all x for which f is defined A weighted type graph is a type graph w
60. r Rights that applies to Your use of the Licensed Material Licensed Material means the artistic or liter ary work database or other material to which the Licensor applied this Public License Licensed Rights means the rights granted to You subject to the terms and conditions of this Public License which are limited to all Copyright and Similar Rights that apply to Your use of the Licensed Material and that the Licensor has authority to license A 3 Creative Commons Attribution 4 0 International Public License h Licensor means the individual s or entity ies granting rights under this Public License i Share means to provide material to the public by any means or process that requires permis sion under the Licensed Rights such as re production public display public performance distribution dissemination communication or importation and to make material available to the public including in ways that members of the public may access the material from a place and at a time individually chosen by them j Sui Generis Database Rights means rights other than copyright resulting from Directive 96 9 EC of the European Parliament and of the Council of 11 March 1996 on the legal protection of databases as amended and or succeeded as well as other essentially equiva lent rights anywhere in the world k You means the individual or entity exercising the Licensed Rights under this Public License Your has a cor
61. rce that includes the required information 3 If requested by the Licensor You must re move any of the information required by Section 3 a 1 A to the extent reasonably practicable 4 If You Share Adapted Material You produce the Adapter s License You apply must not prevent recipients of the Adapted Material from complying with this Public License Section 4 Sui Generis Database Rights Where the Licensed Rights include Sui Generis Database Rights that apply to Your use of the Licensed Material a for the avoidance of doubt Section 2 a 1 grants You the right to extract reuse repro duce and Share all or a substantial portion of the contents of the database b if You include all or a substantial portion of the database contents in a database in which You have Sui Generis Database Rights then the database in which You have Sui Generis Database Rights but not its individual con tents is Adapted Material and A 3 Creative Commons Attribution 4 0 International Public License c You must comply with the conditions in Sec tion 3 a if You Share all or a substantial por tion of the contents of the database For the avoidance of doubt this Section 4 sup plements and does not replace Your obligations un der this Public License where the Licensed Rights include other Copyright and Similar Rights Section 5 Disclaimer of Warranties and Limitation of Liability a Unless otherwise separately undertaken
62. responding meaning Section 2 Scope a License grant 1 Subject to the terms and conditions of this Public License the Licensor hereby grants You a worldwide royalty free non sublicensable non exclusive irrevocable li cense to exercise the Licensed Rights in the Licensed Material to A reproduce and Share the Licensed Ma terial in whole or in part and B produce reproduce and Share Adapted Material 2 Exceptions and Limitations For the avoid ance of doubt where Exceptions and Lim itations apply to Your use this Public Li cense does not apply and You do not need to comply with its terms and conditions 3 Term The term of this Public License is specified in Section 6 a 4 Media and formats technical modifications allowed The Licensor authorizes You to exercise the Licensed Rights in all media and formats whether now known or here after created and to make technical modi fications necessary to do so The Licensor waives and or agrees not to assert any right or authority to forbid You from making tech nical modifications necessary to exercise the Licensed Rights including technical modi fications necessary to circumvent Effective Technological Measures For purposes of this Public License simply making modifi cations authorized by this Section 2 a 4 never produces Adapted Material 5 Downstream recipients A Offer from the Licensor Licensed Ma terial Every recipient of the Lice
63. s graphs and rules and specify when the log window is closed after executing an action The following options can be changed by the user e Layouter Select the layouter which pro duces the initial layout that is determines the initial position of the nodes and edges of the graphs and rules Possible options are Leveled Locate nodes with minimum number of incoming edges at the top nodes directly reachable from those nodes at the level below etc In gen eral produces good results for graphs containing only binary edges Spring embedder Use a spring em bedder to layout graphs and rules In general produces satisfiable results e Rule style Select how rules are displayed Possible options are Separated The left hand side and right hand side are displayed separately and the correspondence morphism is displayed with dashed lines Unified The left hand side and right hand side are displayed in a merged graph colors indicate which nodes and edges are removed and created e Close log when finished During proving comparing or tracing a log is displayed which reports to the user what the algorithms are currently doing This option controls when this log is automatically closed Possible values are Never Never automatically close the log The user must click the Close but ton manually to close the log 12 When successful The log is automati cally closed
64. ser If an algorithm finds a relative termina tion proof all algorithms are stopped and the procedure is repeated on the smaller graph trans formation system from this relative termination proof Algorithms are run concurrently but it is not the case that all algorithms are started at the same time only as many algorithms are run con currently as CPU cores The order in which the algorithms are executed depends on their order in the list There are three possible outcomes of this ac tion a proof that the currently opened graph transformation system terminates a proof that the currently opened graph transformation system does not terminate or if none of the algorithms could find a termination or non termination proof no proof at all 2 6 Specifying algorithms 2 5 2 Comparing algorithms To compare the results of a number of algorithms on the currently opened graph transformation system select the Compare tab from the action panel give a list of algorithm to compare and click the Execute button When comparing algorithms all algorithms specified by the user are run until they finish either by giving a relative or non relative termi nation proof a non termination proof or report that they cannot find a proof The results of all algorithms are reported to the user If some algorithm return a relative termination proof the relative termination proof will be reported and the procedure will not be repeated on the sma
65. set decreases in each rule application This algorithm is described in 5 4 3 e Type graph finder Tries to prove termination by the weighted type graph method described in 85 4 5 The parameters are Number of nodes in type graph maxi mal number of nodes in the type graph Maximum weight maximal weight only available if the Use SMT option is turned off if on there is no limit on the maximum weight Possible semirings which kind of eval uation can be used Use SMT whether to use an external SMT solver click the Configure button to specify which SMT solver to use Use non relative termination whether to use a relative or non relative termi nation If non relative termination is used and the SMT solver fails to find a proof the relative termination is used afterwards e Match bound finder Tries to prove termi nation by using the match bound method described in 85 4 6 The Length limit pa rameter specifies after how many iterations the algorithm will be aborted while the other parameters specify which type graph simpli fications will be used e Petri net approximator Tries to prove ter mination by approximating the graph trans formation system by a Petri net This al gorithm is described in 5 4 4 This algo rithm requires an external SMT solver Click the Configure button to specify which SMT solver to use e External tool Sends the graph transforma tio
66. society un der any voluntary or waivable statutory or compulsory licensing scheme In all other cases the Licensor expressly reserves any right to collect such royalties Section 3 License Conditions Your exercise of the Licensed Rights is expressly made subject to the following conditions a Attribution 38 If You Share the Licensed Material includ ing in modified form You must A retain the following if it is supplied by the Licensor with the Licensed Material i identification of the creator s of the Licensed Material and any oth ers designated to receive attribu tion in any reasonable manner re quested by the Licensor including by pseudonym if designated ii a copyright notice iii a notice that refers to this Public License iv a notice that refers to the disclaimer of warranties v a URI or hyperlink to the Licensed Material to the extent reasonably practicable B indicate if You modified the Licensed Material and retain an indication of any previous modifications and C indicate the Licensed Material is li censed under this Public License and include the text of or the URI or hyper link to this Public License 2 You may satisfy the conditions in Sec tion 3 a 1 in any reasonable manner based on the medium means and context in which You Share the Licensed Material For example it may be reasonable to sat isfy the conditions by providing a URI or hyperlink to a resou
67. stem is terminating Formally annotating a graph transformation system is done by constructing a new graph trans formation systems which uses A x N as label set where A is the label set of the original system When an occurrence of a left hand side is replaced by a right hand side the new edges are annotated with a creation height which is equal to the small est creation height of the left hand side plus one Now the termination argument is as follows if there exists a type graph with annotated edges 30 for the annotated graph transformation system then the match bound is bounded because the type graph is finite by definition and thus the original graph transformation system is terminat ing See 3 for more details and formal definitions and proofs Grez s match bound algorithm uses the follow ing algorithm to try to find a type graph for the annotated graph transformation system 1 Start with the flower graph that is the graph which consists of a single node v and for each label and edge which is only connected as many times as the arity prescribes to v All edges are annotated with the creation height 0 2 Find an occurrence of an annotated left hand side in the current type graph If such an occurrence exists extend the type graph with the right hand side The left hand side is not removed from the type graph Note that the annotations of all edges in the right hand side is the minimum annotation of the left h
68. terface 13 CONTENTS 3 1 Using Grez from the command line 2 a ee 13 3 2 Command line options 2 2 m nn nn 13 3 2 1 General options 2 2 20 02 00 0 13 3 2 2 Action type and system selection 2 2 oo ee 14 3 2 3 Reporting and proof generation 2 0 020 0004 14 3 2 4 Random system generation 0000000 eee eee 14 3 3 Specifying algorithms 15 4 Specifying Graph Transformation Systems The Simple Graph Format 17 4 1 A first tours e a a A Be 17 4 1 1 Defining rules 2 222222 on nn nn 17 4 1 2 Defining graph transformation systems 2 2 2 nn nenn 18 4 2 Grammar es ars eR eae a EE Soe Be aOR ee OE Ok Ae OOS 19 4 2 1 TOKENS osos e ee de eee ee 19 4 2 2 Object definitions 2 0 nn 19 4 2 3 Gras 20 4 2 4 Morphisms 2 2 nn nn 20 4 2 5 Transformation rules 2 2 00 0000 ee 21 4 2 6 Transformation systems 000000 eee ee 21 4 3 Examples 24 2c 4 6 2h RR bee RR eee ee eh 22 4 3 1 Two systems in one file 000000 2 eee eee 22 4 3 2 In place definition o 22 4 33 Ad ho routing 20 2246 0 66 oe bee ee eee be ee nen 23 5 Theoretical Foundations 25 5 1 Graph transformation a 25 5 2 Termination Sire ogee ak eh RSE ee Ee OS eee ee he SE GE ae 26 5 3 Satisfiability modulo theories 2 2 0 e 27 5 4 Algorithms for proving termination and non termination 27 5 4 1 Finding cycles 27 5 4 2 N
69. ternatively press the Edit button to edit the signature through a dialog Left hand and right hand side parameters e Number of nodes Distribution for the num ber of nodes in a graph see below Density Distribution for the density of the graph The density is a floating point number gt 0 which determines the number of edges in the graph depending on the number of nodes In particular if n is the number of nodes and d the density the number of edges in the graph will be d n In typical cases the density will lie between 0 and 1 Connectedness This parameter control to which extend the graph is connected It has three possible values 2 THE GRAPHICAL USER INTERFACE Arbitrary All graphs can be gener ated regardless of whether they are connected or not No isolated nodes Non connected graphs can be generated but each node will always be incident to at least one edge Connected Only connected graphs will be generated Interface parameters e Number of nodes Distribution for the num ber of nodes in the interface see below e Discrete interfaces When checked only interfaces without edges will be generated Otherwise the interface will be the maximal interface such that each interface edge of the left hand side has a corresponding edge in the right hand side Specifying distributions Distributions can be given through a dialog by clicking the Edit but ton or entered manually by
70. ting 27 28 NodeCounter 15 non uniform termination see termination Number of rules parameter 7 Open GTS menu item 6 7 Options menu 6 outgoing edge factorization see edge factor ization Petri net approximation 28 Petri net approximation algorithm 10 15 28 44 PetriNet 15 Prove action 8 relative termination see termination Remove button 9 rule 25 26 rule 17 21 rule display 5 rule selection box 5 satisfiability modulo theories 2 21 SGF see simple graph format signature 25 Signature parameter 7 simple graph format 17 23 comment 19 defining edges 18 20 defining graph transformation systems 18 19 21 22 defining morphisms 20 21 defining nodes 18 20 defining rules 17 18 21 identifier 19 keyword 19 SMT see satisfiability modulo theories SMT solver 10 11 SMT solvers menu item 6 status bar 6 System menu 6 7 termination 1 26 27 non uniform 26 relative 26 uniform 26 termination tool 10 11 Termination tools menu item 6 to 20 Trace action 9 tropical evaluation 29 type graph 29 type graph algorithm 10 15 29 TypeGraph 15 uniform termination see termination Index Visit website menu item 7 1 weighted type graph 29 45
71. vative Works within the Source form or documentation if provided along with the Derivative Works or within a display generated by the Derivative Works if and wherever such third party notices nor mally appear The contents of the NOTICE file are for informational purposes only and do not modify the License You may add Your own at tribution notices within Derivative Works that You distribute alongside or as an addendum to the NOTICE text from the Work provided that such additional attribution notices cannot be construed as modifying the License You may add Your own copyright statement to Your modifications and may provide additional or different license terms and conditions for use reproduction or distribution of Your mod ifications or for any such Derivative Works as a whole provided Your use reproduction and distribution of the Work otherwise complies with the conditions stated in this License 5 Submission of Contributions Unless You explicitly state otherwise any Contribution in tentionally submitted for inclusion in the Work by You to the Licensor shall be under the terms and conditions of this License without any addi tional terms or conditions Notwithstanding the above nothing herein shall supersede or modify the terms of any separate license agreement you may have executed with Licensor regarding such Contributions 6 Trademarks This License does not grant permission to use the trade names trademarks
72. while the second is distributed under the Apache license see Appendix A 2 This documentation is distributed under the Creative Commons 4 0 Attribution licence CC BY 4 0 see Appendix A 3 Two The Graphical User Interface The most common way to interact with Grez is the graphical user interface which is presented in this chapter The graphical user interface allows the user to open graph transformation systems and generate random ones run algorithms which try to prove termination or non termination and inspect termination and non termination proofs produced by these algorithms Additionally the graphical user interface is used to configure the external tools called by Grez 2 1 Running Grez To run Grez a working Java 8 installation must be present If this is the case Grez s graphical user interface GUI is started on the command line by changing to the directory where the file grez jar resides and issuing the command java jar grez jar Alternatively in most operating systems one can double click the grez jar file in the file browser When starting Grez s graphical user interface one can also specify an input file and use the command line option system to open a specific graph transformation system see 3 2 2 2 The main window The main window of Grez is displayed in Fig ure 2 1 It consists of the following parts from top to bottom these are e In the main menu there are various com
73. xternal Java libraries 1 Some SMT solvers that claim to support the SMT LIB 2 format actually do not fully do so e ANTLR 4 www antlr org used for pars ing the output of SMT solvers e Google Guava version 14 or newer github com google guava 1 5 Installation To install Grez it is only needed to copy the file grez jar to a location of your choice If you plan on using Grez through the command line a lot it is advisable to create a shell script in a directory in the path In Unix like operating systems such as Mac OS X and Linux this file could be named grez and contain bin sh java jar Dgrez script grez path to grez jar 0 the last two lines should be on the same line In Windows the file could be named grez bat and look like java jar Dgrez script grez C path to grez jar the file should consist of a single line The Dgrez script grez option sets a Java prop erty which is read by Grez It has no effect to the working of the program except that the command name is displayed correctly in some user interactions Creating such a shell script allows you to use grez as a command instead of java jar grez jar 1 6 Feedback and bug reports Grez is free software both as in free speech and as in free beer This means that you can use the software and inspect and modify its source code without cost but it also means that there is no warranty no guarantee and no customer support 1

Download Pdf Manuals

Related Search

Related Contents

User Manual ROM-DB3900    User Manual - Touch Screens Inc.  取扱説明書 - M  Mode d`emploi - Supertoinette  

Copyright © All rights reserved. Failed to retrieve file