(* To evaluate code of the editor in the interpreter: select the code lines to evaluate and press CTRL+E (or CMD+E on MacOS). *) (* All demos on completion algorithm are at the end of the file. *) (* We start by basic functionalities on tree automata and regular tree expressions *) (* Tree automata definition and manipulation in Taml *) let alp= alphabet "f:2 a:0 b:0 c:0";; let aut= automaton alp "States q0 q1 q2 Final States q0 Transitions f(q1,q0) -> q0 f(q1,q1) -> q2 a -> q1 q2 -> q0";; let vars= variables "X Y Z";; (* TRS *) let trs1= trs alp vars ["f(X,f(Y,Z)) -> f(Y,Z)";"f(a,a) -> b"];; let ts= term_list alp vars ["a";"f(a,a)";"f(f(a,a),a)";"f(a,f(a,a))";"f(f(a,a),f(a,a))"];; (* Filtering a list of terms w.r.t. a tree automaton *) let reco= filter ts aut;; (* Computing the complement of a tree automaton *) let aut_inverse= inverse aut;; (* Generating terms recognized by a tree automaton *) let ts3= gen_terms aut 4;; let ts4= gen_terms aut_inverse 4;; filter ts4 aut;; (* Regular Tree Expressions *) let r1= regexp alp "f(a, ((f(a, c) * c) . c (a)))";; (* Regular Tree Expressions to tree automaton *) let aut_r1= regexp_to_automaton r1;; (* Equality between languages *) is_equal aut aut_r1;; (* Simplified Regular Tree Expressions *) let sr1= sregexp alp "f(a,[f(a,*|a)])";; let r2= sregexp_to_regexp sr1;; (* Simplified Regular Tree Expressions to Tree Automaton *) let aut_sr1= sregexp_to_automaton sr1;; is_equal aut aut_sr1;; (* Automaton of normal forms of a TRS *) let irr_trs1= irr alp trs1;; (* Call to basic Timbuk completion *) let (completed_automaton,is_complete,pattern_found)= timbuk_completion 10 aut trs1 [] [] false;; (* Simplification of an intersection between reachable terms and normal forms *) let nf= simplify (inter irr_trs1 completed_automaton);; (* Get components from a Timbuk specification file *) let (aut_list,trs,eq_list,term_list)= read_file "delete.txt";; (* Get the first and second automaton from the automaton list *) let (a::atc::_) = aut_list;; (* Run Timbuk completion in functional mode, with ground equation generation on a and atc. permits to obtain the completed automaton in Taml *) let (generated_equations,completed_automaton,is_complete)= timbuk_fun_completion 30 a atc trs term_list;; (* See all Taml's functions *) help();; (* -------------- Completion demos ------------------------- *) (* Run Timbuk's completion on several files, enclosed in the local file system *) (* See what are the available files *) Sys.readdir(".");; (* Print the content of a Timbuk specification file *) print_file "delete.txt";; (* Run Timbuk in functional mode, with ground equation generation, on the insertionSort.txt file all other .txt files can be used *) timbuk_cmd "--fung 30 delete.txt";; (* Higher-order functions *) print_file "insertionSort.txt";; timbuk_cmd "--fung 30 insertionSort.txt";; print_file "mapPlus.txt";; timbuk_cmd "--fung 30 mapPlus.txt";; (* may take some time in the online version *) print_file "filterEven.txt";; timbuk_cmd "--fung 30 filterEvent.txt";; (* Run Sys.readdir(".") to see what are the other available examples *) Sys.readdir(".");;

Timbuk Online

This is an online demonstration of the Timbuk framework.

Timbuk is a collection of tools for achieving proofs of reachability over Term Rewriting Systems and for manipulating Tree Automata. Timbuk can be used for program verification. For instance, it is used to verify Higher-Order Functional Programs, Java programs and Cryptographic Protocols (see some papers and in the examples of the distribution).

Editor commands

Command	Effect
Ctrl + E	Execute selected code
Ctrl + O	Open file
Ctrl + S	Save file
Ctrl + N	New file

Toplevel commands

Command	Effect
Enter / Return	Submit code
Up / Down	Cycle through history
`help ()`	Print help