==================================================================== == CYCSRS: Transforming Cycle Termination into String Termination == ==================================================================== PURPOSE ======= CYCSRS is a tool that can * transform a cycle rewrite system (given as string rewrite in WST format) into a string rewrite system, s.t. termination is unchanged. That is the cycle rewrite system is cycle terminating if and only if the transformed system is string terminating. The tool provides three such sound and complete encodings, called split, rotate, and shift. * prove cycle termination by using direct techniques (without transformation) by running the termination prover torpacyc or by running the termination provers AProVE or TTT2 on the transformed problem. To use these tools they must be installed from the corresponding websites (see REQUIREMENTS). Moreover, the file conf.sh must be adjusted, s.t. CYCRSRS can find these tools. BUILDING CYCSRS =============== CYCSRS is 'cabalized' which automates the build process of Haskell-programs. A recent version of the Haskell-Platform already includes the cabal program. The Haskell platform can be downloaded from http://www.haskell.org/platform/ To build CYCSRS execute cabal configure cabal build This builds the CYCSRS executable in dist/build/CYCSRS/CYCSRS Copy the executable TOGETHER with the delivered bash-script conf.sh into one folder. Adjust the pathes in conf.sh to match the pathes of your local installation of other tools. For using CYCSRS as transformation tool only no other tools are required. typing ./CYCSRS help will print detailed usage information to stdout (which can also be found at the end of this file) REQUIREMENTS ============ Building: Building of CYCSRS requires a recent installation of the Haskell platform. Execution: To use all features of CYCSRS the following tools must be installed on your local system: * bash : http://www.gnu.org/software/bash/ since CYCSRS uses bash scripts for executing other tools, bash must be installed on your system * torpacyc version 2015 : http://www.win.tue.nl/~hzantema/torpa.html the automatic termination prover for cycle rewrite systems developed by Hans Zantema * AProVE : http://aprove.informatik.rwth-aachen.de the command line version of the termination prover AProVE is required. * TTT2 : http://cl-informatik.uibk.ac.at/software/ttt2/index.php the comand line version of the Tyrolean Termination Tool 2 * minisat : http://minisat.se several of the provers require the SAT-Solver minisat * Yices 1 : http://yices.csl.sri.com/ required by torpacyc version 2014 and by AProVE * Yices 2 : http://yices.csl.sri.com/ required by torpacyc version 2015 * Z3 : http://z3.codeplex.com/ AProVE requires the SMT-solver Z3 * Java JDK : http://www.oracle.com/technetwork/java/javase/downloads/index.html required to execute AProVE USAGE AVAILABLE OPTIONS * CYCSRS encode OUTPUTFORMAT ENCODINGS INFILE [-oOUTFILE] Encode the string rewrite system in INFILE and print the encoded string rewrite system on stdout (or write output to OUTFILE if provided by -o) * CYCSRS prove TOOL OUTPUTOPT ENCODINGS INFILE [-tTIMEOUT] Prove termination of the encoded string or cycle rewrite relation. An optional timeout in seconds can be set * CYCSRS statistic ENCODINGS INFILE Print statistics of the encoded string rewrite system * CYCSRS help Show help ENCODINGS a sequence of encodings applied to the input from left to right (separated by whitespaces, without quotes, e.g. srscyc split ) available encodings are: none = no encoding is applied split = encode cycle into string rewriting by splitting the rules rotate = encode cycle into string rewriting by rotation and prefix rewriting shift = encode cycle into string rewriting by shifting and rewriting srscyc = encode string rewriting into cycle rewriting OUTPUTFORMAT available formats are: srs = string rewrite system in text format trs = term rewrite system in text format TOOL select the tool to prove termination !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!! ENSURE that the NECESSARY SOFTWARE is installed and !!! !!! ADJUST the pathes to your LOCAL CONFIGURATION in the file !!! !!! !!! !!! conf.sh !!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! available tools are: torpacyc = proves cycle termination by matrix interpretations aprove = termination prover AProVE ttt2 = termination prover TTT2 combA1 = first torpacyc2 and if necessary the encoding split is applied to the remaining termination problem and then AProVE is called combA2 = first AProVE is applied to check for cycle nontermination, then torpacyc2 and then split together with AProVE are applied combT1 = first torpacyc2 and if necessary the encoding split is applied to the remaining termination problem and then TTT2 is called combT2 = first TTT2 is applied to check for cycle nontermination, then torpacyc2 and then split together with TTT2 are applied OUTPUTOPT simple = only print the answer (yes/no/maybe) long = verbose output including input, output of prover asf. tabbed = print the internal command, the answer, the time, separated by tabs INFILE the format of the content is resolved by its file extension .srs = string rewrite system in text format .xml = string rewrite system in XML format of the TPDB TIMEOUT a number of seconds Configuration ============= the available parameters can be adjusted in the file conf.sh Examples ======== * CYCSRS encode trs srscyc split myinfile.srs -omyoutfile encodes the SRS in myinfile.srs by applying first the transformation srscyc and thereafter the transformation split. The generated rewrite system is written as a term rewrite system into myoutfile * CYCSRS prove torpacyc long none myinfile.xml -t60 proves cycle termination of the SRS in myinfile.xml using torpacyc with long output and a timeout of 60sec. * CYCSRS prove aprove simple split myinfile.srs proves cycle termination of the SRS in myinfile.srs by first transforming the system using the split-transformation and then running the prover prover AProVE on the generated SRS with no timeout