From 22ad9f5ed257f3d10506fb69e110607a0639b990 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 9 Aug 2018 14:39:11 +0200 Subject: [PATCH 01/23] org: show some useful R operations on ltlcross output * doc/org/ltlcross.org: Here. * doc/org/init.el.in, doc/org/.dir-locals.el.in: Enable R, and install ess. --- doc/org/.dir-locals.el.in | 2 + doc/org/init.el.in | 18 +- doc/org/ltlcross.org | 391 +++++++++++++++++++++++++------------- 3 files changed, 276 insertions(+), 135 deletions(-) diff --git a/doc/org/.dir-locals.el.in b/doc/org/.dir-locals.el.in index 8f12291e9..fcc80f346 100644 --- a/doc/org/.dir-locals.el.in +++ b/doc/org/.dir-locals.el.in @@ -31,12 +31,14 @@ (python . t) (plantuml . t) (dot . t) + (R . t) (C . t))))) (org-confirm-babel-evaluate . nil) (org-plantuml-jar-path . "@abs_top_builddir@/doc/org/plantuml.jar") (org-babel-python-command . "@PYTHON@") (org-babel-C++-compiler . "./g++wrap") (shell-file-name . "@SHELL@") + (ess-ask-for-ess-directory . nil) (org-export-html-postamble . nil) (org-babel-default-header-args:plantuml . ((:results . "file") diff --git a/doc/org/init.el.in b/doc/org/init.el.in index b434dedfc..b515d31a7 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -29,11 +29,17 @@ (let ((org-p-c (cadr (assq 'org-plus-contrib package-archive-contents)))) (package-install org-p-c))) -(unless (require 'htmlize nil t) - (add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t) - (package-refresh-contents) - (let ((htmlize (cadr (assq 'htmlize package-archive-contents)))) - (package-install htmlize))) +(let ((have-htmlize (require 'htmlize nil t)) + (have-ess (require 'ess nil t))) + (unless (and have-htmlize have-ess) + (add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t) + (package-refresh-contents) + (unless have-htmlize + (let ((htmlize (cadr (assq 'htmlize package-archive-contents)))) + (package-install htmlize))) + (unless have-ess + (let ((ess (cadr (assq 'ess package-archive-contents)))) + (package-install ess))))) (require 'ox-publish) (require 'org-install) @@ -54,6 +60,7 @@ (dot . t) (python . t) (plantuml . t) + (R . t) (C . t))) (setq org-confirm-babel-evaluate nil) (setq org-plantuml-jar-path "@abs_top_builddir@/doc/org/plantuml.jar") @@ -65,6 +72,7 @@ (setq org-babel-python-command "@PYTHON@") (setq org-babel-C++-compiler "./g++wrap") (setq shell-file-name "@SHELL@") +(setq ess-ask-for-ess-directory nil) (setq org-babel-default-header-args:plantuml '((:results . "file") diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index bb46b4b0d..a5d920d71 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -13,7 +13,7 @@ The main differences with LBTT are: - *support for PSL formulas in addition to LTL* - support for (non-alternating) automata with *any type of acceptance condition*, - support for *weak alternating automata*, - - additional intersection *checks with the complement*, allowing + - additional intersection *checks with the complement* (option =-D=), allowing to check equivalence of automata more precisely, - *more statistics*, especially: - the number of logical transitions represented by each physical edge, @@ -21,7 +21,7 @@ The main differences with LBTT are: - the number of SCCs with their various strengths (nonaccepting, terminal, weak, strong) - the number of terminal, weak, and strong automata - an option to *reduce counterexample* by attempting to mutate and - shorten troublesome formulas, + shorten troublesome formulas (option =--grind=), - statistics output in *CSV* for easier post-processing, - *more precise time measurement* (LBTT was only precise to 1/100 of a second, reporting most times as "0.00s"). @@ -229,6 +229,131 @@ of untrusted references. The easiest way to observe the effect of =--reference= is to run the =ltlcross= with the [[#verbose][=--verbose= option]], with and without some =--reference= translators. +* Detecting problems + :PROPERTIES: + :CUSTOM_ID: checks + :END: + +If a translator exits with a non-zero status code, or fails to output +an automaton =ltlcross= can read, and error will be displayed and the +result of the translation will be discarded. + +Otherwise =ltlcross= performs the following checks on all translated +formulas ($P_i$ and $N_i$ designate respectively the translation of +positive and negative formulas by the ith translator). + + - Intersection check: $P_i\otimes N_j$ must be empty for all + pairs of $(i,j)$. + + A single failing translator might generate a lot of lines of + the form: + + : error: P0*N1 is nonempty; both automata accept the infinite word: + : cycle{p0 & !p1} + : error: P1*N0 is nonempty; both automata accept the infinite word: + : p0; !p1; cycle{p0 & p1} + : error: P1*N1 is nonempty; both automata accept the infinite word: + : p0; cycle{!p1 & !p0} + : error: P1*N2 is nonempty; both automata accept the infinite word: + : p0; !p1; cycle{p0 & p1} + : error: P1*N3 is nonempty; both automata accept the infinite word: + : p0; !p1; cycle{p0 & p1} + : error: P1*N4 is nonempty; both automata accept the infinite word: + : p0; cycle{!p1 & !p0} + : error: P2*N1 is nonempty; both automata accept the infinite word: + : p0; !p1; !p0; cycle{!p1 & !p0; p0 & !p1; !p1; !p1; p0 & !p1} + : error: P3*N1 is nonempty; both automata accept the infinite word: + : p0; !p1; !p1 & !p0; cycle{p0 & !p1} + : error: P4*N1 is nonempty; both automata accept the infinite word: + : p0; !p1; !p1 & !p0; cycle{p0 & !p1} + + In this example, translator number =1= looks clearly faulty + (at least the other 4 translators do not contradict each other). + + Examples of infinite words that are accepted by both automata + always have the form of a lasso: a (possibly empty) finite prefix + followed by a cycle that should be repeated infinitely often. + The cycle part is denoted by =cycle{...}=. + + - Complemented intersection check. If $P_i$ and $N_i$ are + deterministic, =ltlcross= builds their complements, $Comp(P_i)$ + and $Comp(N_i)$, and then ensures that $Comp(P_i)\otimes + Comp(N_i)$ is empty. If only one of them is deterministic, for + instance $P_i$, we check that $P_j\otimes Comp(P_i)$ for all $j + \ne i$; likewise if it's $N_i$ that is deterministic. + + By default this check is only done for deterministic automata, + because complementation is relatively cheap is that case (at least + it is cheap for simple acceptance conditions). Using option + =--determinize=, =ltlcross= can be instructed to perform + complementation of non-deterministic automata as well, ensuring + precise equivalence checks between all automata. However be aware + that this determinization + complementation may generate large + automata. + + When validating a translator with =ltlcross= without using the + =--determinize= option we highly recommend to include a translator + with good deterministic output to augment test coverage. Using + '=ltl2tgba -lD %f >%O=' will produce deterministic automata for + all obligation properties and many recurrence properties. Using + '=ltl2dstar --ltl2nba=spin:pathto/ltl2tgba@-Ds %L %O=' will + systematically produce a deterministic Rabin automaton (that + =ltlcross= can complement easily). + + - Cross-comparison checks: for some state-space $S$, + all $P_i\otimes S$ are either all empty, or all non-empty. + Similarly all $N_i\otimes S$ are either all empty, or all non-empty. + + A cross-comparison failure could be displayed as: + + : error: {P0,P2} disagree with {P1} when evaluating the state-space + : the following word(s) are not accepted by {P1}: + : P0 accepts: p0 & !p1 & !p2 & p3; p0 & p1 & !p2 & p3; p0 & p1 & p2 & p3; cycle{p0 & p1 & p2 & p3; p0 & p1 & !p2 & !p3; p0 & p1 & p2 & !p3; p0 & p1 & !p2 & !p3} + : P2 accepts: p0 & !p1 & !p2 & p3; cycle{p0 & p1 & !p2 & !p3; p0 & p1 & p2 & p3; p0 & p1 & !p2 & p3} + + If =--products=N= is used with =N= greater than one, the number of + the state-space is also printed. This number is of no use by + itself, except to explain why you may get multiple disagreement + between the same sets of automata. + + These products tests may sometime catch errors that were not + captured by the first two tests if one non-deterministic automaton + recognize less words than what it should. If the input automata + are deterministic or the =--determinize= option is used, this test + is redundant and can be disabled. (In fact, the =--determinize= + option implies option =--product=0= to do so.) + + - Consistency check: + + For each $i$, the products $P_i\otimes S$ and $N_i\otimes S$ + actually cover all states of $S$. Because $S$ does not have any + deadlock, any of its infinite path must be accepted by $P_i$ or + $N_i$ (or both). + + An error in that case is displayed as + + : error: inconsistency between P1 and N1 + + If =--products=N= is used with =N= greater than one, the number of + the state-space in which the inconsistency was detected is also + printed. + + This test may catch errors that were not captured by the first two + tests if one non-deterministic automaton recognize less words than + what it should. If the input automata are deterministic or the + =--determinize= option is used, this test is redundant and can be + disabled. (In fact, the =--determinize= option implies option + =--product=0= to do so.) + +The above checks are similar to those that are performed by [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], +except for the complemented intersection check, which is only done in +=ltlcross=. + +If any problem was reported during the translation of one of the +formulas, =ltlcheck= will exit with an exit status of =1=. Statistics +(if requested) are output nonetheless, and include any faulty +automaton as well. + * Getting statistics Detailed statistics about the result of each translation, and the @@ -592,15 +717,15 @@ configurations, and the strings =ltl2tgba -s --small %f >%O= and ltlcross -f a -f Ga 'ltl2tgba -s --small %f >%O' 'ltl2tgba -s --deter %f >%O' --csv #+END_SRC #+RESULTS: -: "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc" -: "(a)","ltl2tgba -s --small %f >%O","ok",0,0.043876,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4208,2 -: "(a)","ltl2tgba -s --deter %f >%O","ok",0,0.0432137,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4208,2 -: "(!(a))","ltl2tgba -s --small %f >%O","ok",0,0.0400653,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4205,2 -: "(!(a))","ltl2tgba -s --deter %f >%O","ok",0,0.0450417,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4205,2 -: "(G(a))","ltl2tgba -s --small %f >%O","ok",0,0.0429628,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2077,1 -: "(G(a))","ltl2tgba -s --deter %f >%O","ok",0,0.0478663,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2077,1 -: "(!(G(a)))","ltl2tgba -s --small %f >%O","ok",0,0.0436822,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8442,2 -: "(!(G(a)))","ltl2tgba -s --deter %f >%O","ok",0,0.039919,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8442,2 +: "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nondet_states","nondet_aut","complete_aut","product_states","product_transitions","product_scc" +: "a","ltl2tgba -s --small %f >%O","ok",0,0.0129968,2,2,3,1,2,0,0,0,201,4144,2 +: "a","ltl2tgba -s --deter %f >%O","ok",0,0.0116347,2,2,3,1,2,0,0,0,201,4144,2 +: "!(a)","ltl2tgba -s --small %f >%O","ok",0,0.0127019,2,2,3,1,2,0,0,0,201,4149,2 +: "!(a)","ltl2tgba -s --deter %f >%O","ok",0,0.0117374,2,2,3,1,2,0,0,0,201,4149,2 +: "G(a)","ltl2tgba -s --small %f >%O","ok",0,0.0126186,1,1,1,1,1,0,0,0,200,2059,1 +: "G(a)","ltl2tgba -s --deter %f >%O","ok",0,0.011645,1,1,1,1,1,0,0,0,200,2059,1 +: "!(G(a))","ltl2tgba -s --small %f >%O","ok",0,0.0129519,2,3,4,1,2,0,0,1,400,8264,2 +: "!(G(a))","ltl2tgba -s --deter %f >%O","ok",0,0.0129941,2,3,4,1,2,0,0,1,400,8264,2 To present these results graphically, or even when analyzing these data, it might be convenient to give each configured tool a shorter @@ -610,143 +735,149 @@ form "={short name}actual command=". For instance: #+BEGIN_SRC sh :results verbatim :exports both -ltlcross -f a -f Ga '{small} ltl2tgba -s --small %f >%O' '{deter} ltl2tgba -s --deter %f >%O' --csv +genltl --and-f=1..5 | +ltlcross '{small} ltl2tgba -s --small %f >%O' \ + '{deter} ltl2tgba -s --deter %f >%O' --csv=ltlcross.csv +cat ltlcross.csv #+END_SRC #+RESULTS: -: "formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","product_states","product_transitions","product_scc" -: "(a)","small","ok",0,0.0433468,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4208,2 -: "(a)","deter","ok",0,0.0429179,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4208,2 -: "(!(a))","small","ok",0,0.0400513,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4205,2 -: "(!(a))","deter","ok",0,0.040167,2,2,3,1,2,1,1,0,0,0,0,1,0,0,201,4205,2 -: "(G(a))","small","ok",0,0.0447826,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2077,1 -: "(G(a))","deter","ok",0,0.0439892,1,1,1,1,1,0,0,1,0,0,0,0,1,0,200,2077,1 -: "(!(G(a)))","small","ok",0,0.0444007,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8442,2 -: "(!(G(a)))","deter","ok",0,0.0396312,2,3,4,1,2,1,1,0,0,0,0,1,0,0,400,8442,2 +#+begin_example +"formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nondet_states","nondet_aut","complete_aut","product_states","product_transitions","product_scc" +"F(p1)","small","ok",0,0.0138108,2,3,4,1,2,0,0,1,400,8272,3 +"F(p1)","deter","ok",0,0.0142178,2,3,4,1,2,0,0,1,400,8272,3 +"!(F(p1))","small","ok",0,0.013972,1,1,1,1,1,0,0,0,200,2055,2 +"!(F(p1))","deter","ok",0,0.0139471,1,1,1,1,1,0,0,0,200,2055,2 +"(F(p1)) & (F(p2))","small","ok",0,0.0136648,4,9,16,1,4,0,0,1,798,16533,5 +"(F(p1)) & (F(p2))","deter","ok",0,0.0140229,4,9,16,1,4,0,0,1,798,16533,5 +"!((F(p1)) & (F(p2)))","small","ok",0,0.0144659,3,5,7,1,3,0,0,0,598,7367,4 +"!((F(p1)) & (F(p2)))","deter","ok",0,0.0143098,3,5,7,1,3,0,0,0,598,7367,4 +"(F(p1)) & (F(p2)) & (F(p3))","small","ok",0,0.0142109,8,27,64,1,8,0,0,1,1587,33068,34 +"(F(p1)) & (F(p2)) & (F(p3))","deter","ok",0,0.0149064,8,27,64,1,8,0,0,1,1587,33068,34 +"!((F(p1)) & (F(p2)) & (F(p3)))","small","ok",0,0.0159551,4,6,24,1,4,1,1,0,601,6171,4 +"!((F(p1)) & (F(p2)) & (F(p3)))","deter","ok",0,0.0143288,7,19,37,1,7,0,0,0,1387,18792,33 +"(F(p1)) & (F(p2)) & (F(p3)) & (F(p4))","small","ok",0,0.0152539,16,81,256,1,16,0,0,1,2727,57786,74 +"(F(p1)) & (F(p2)) & (F(p3)) & (F(p4))","deter","ok",0,0.0155381,16,81,256,1,16,0,0,1,2727,57786,74 +"!((F(p1)) & (F(p2)) & (F(p3)) & (F(p4)))","small","ok",0,0.015231,5,8,64,1,5,1,1,0,801,8468,5 +"!((F(p1)) & (F(p2)) & (F(p3)) & (F(p4)))","deter","ok",0,0.0157937,15,65,175,1,15,0,0,0,2527,37226,73 +"(F(p1)) & (F(p2)) & (F(p3)) & (F(p4)) & (F(p5))","small","ok",0,0.017919,32,243,1024,1,32,0,0,1,5330,114068,350 +"(F(p1)) & (F(p2)) & (F(p3)) & (F(p4)) & (F(p5))","deter","ok",0,0.0167644,32,243,1024,1,32,0,0,1,5330,114068,350 +"!((F(p1)) & (F(p2)) & (F(p3)) & (F(p4)) & (F(p5)))","small","ok",0,0.0187427,6,10,160,1,6,1,1,0,1000,10707,6 +"!((F(p1)) & (F(p2)) & (F(p3)) & (F(p4)) & (F(p5)))","deter","ok",0,0.0183562,31,211,781,1,31,0,0,0,5130,82897,349 +#+end_example -* Detecting problems - :PROPERTIES: - :CUSTOM_ID: checks - :END: +In this last example, we saved the CSV output to =ltlcross.csv= so we +can play with it in the next section. -If a translator exits with a non-zero status code, or fails to output -an automaton =ltlcross= can read, and error will be displayed and the -result of the translation will be discarded. +** Working with these CSV files in R -Otherwise =ltlcross= performs the following checks on all translated -formulas ($P_i$ and $N_i$ designate respectively the translation of -positive and negative formulas by the ith translator). +The produced CSV should be directly readable by R's CSV input functions like +=read.csv()=, =readr::read_csv()=, or =data.table::fread()=. - - Intersection check: $P_i\otimes N_j$ must be empty for all - pairs of $(i,j)$. +#+BEGIN_SRC R :session :results output :exports both +library(data.table) +dt <- fread('ltlcross.csv') +str(dt) +#+END_SRC +#+RESULTS: +#+begin_example +Classes ‘data.table’ and 'data.frame': 20 obs. of 16 variables: + $ formula : chr "F(p1)" "F(p1)" "!(F(p1))" "!(F(p1))" ... + $ tool : chr "small" "deter" "small" "deter" ... + $ exit_status : chr "ok" "ok" "ok" "ok" ... + $ exit_code : int 0 0 0 0 0 0 0 0 0 0 ... + $ time : num 0.0133 0.0133 0.0139 0.0128 0.0144 ... + $ states : int 2 2 1 1 4 4 3 3 8 8 ... + $ edges : int 3 3 1 1 9 9 5 5 27 27 ... + $ transitions : int 4 4 1 1 16 16 7 7 64 64 ... + $ acc : int 1 1 1 1 1 1 1 1 1 1 ... + $ scc : int 2 2 1 1 4 4 3 3 8 8 ... + $ nondet_states : int 0 0 0 0 0 0 0 0 0 0 ... + $ nondet_aut : int 0 0 0 0 0 0 0 0 0 0 ... + $ complete_aut : int 1 1 0 0 1 1 0 0 1 1 ... + $ product_states : int 400 400 200 200 798 798 598 598 1587 1587 ... + $ product_transitions: int 8272 8272 2055 2055 16533 16533 7367 7367 33068 33068 ... + $ product_scc : int 3 3 2 2 5 5 4 4 34 34 ... + - attr(*, ".internal.selfref")= +#+end_example - A single failing translator might generate a lot of lines of - the form: +Currently the data frame shows one line per couple (formula, tool). +This makes comparing tools quite difficult, as their results are on +different lines. - : error: P0*N1 is nonempty; both automata accept the infinite word: - : cycle{p0 & !p1} - : error: P1*N0 is nonempty; both automata accept the infinite word: - : p0; !p1; cycle{p0 & p1} - : error: P1*N1 is nonempty; both automata accept the infinite word: - : p0; cycle{!p1 & !p0} - : error: P1*N2 is nonempty; both automata accept the infinite word: - : p0; !p1; cycle{p0 & p1} - : error: P1*N3 is nonempty; both automata accept the infinite word: - : p0; !p1; cycle{p0 & p1} - : error: P1*N4 is nonempty; both automata accept the infinite word: - : p0; cycle{!p1 & !p0} - : error: P2*N1 is nonempty; both automata accept the infinite word: - : p0; !p1; !p0; cycle{!p1 & !p0; p0 & !p1; !p1; !p1; p0 & !p1} - : error: P3*N1 is nonempty; both automata accept the infinite word: - : p0; !p1; !p1 & !p0; cycle{p0 & !p1} - : error: P4*N1 is nonempty; both automata accept the infinite word: - : p0; !p1; !p1 & !p0; cycle{p0 & !p1} +A common transformation is to group the results of all tools on the +same line: using exactly one line per formula. This is easily +achieved using =dcast()= from the =data.table= library. - In this example, translator number =1= looks clearly faulty - (at least the other 4 translators do not contradict each other). +#+BEGIN_SRC R :session :results output :exports both +dt2 <- dcast(dt, formula ~ tool, value.var=names(dt)[-(1:2)], sep=".") +str(dt2) +#+END_SRC - Examples of infinite words that are accepted by both automata - always have the form of a lasso: a (possibly empty) finite prefix - followed by a cycle that should be repeated infinitely often. - The cycle part is denoted by =cycle{...}=. +#+RESULTS: +#+begin_example +Classes ‘data.table’ and 'data.frame': 10 obs. of 29 variables: + $ formula : chr "!((F(p1)) & (F(p2)) & (F(p3)) & (F(p4)) & (F(p5)))" "!((F(p1)) & (F(p2)) & (F(p3)) & (F(p4)))" "!((F(p1)) & (F(p2)) & (F(p3)))" "!((F(p1)) & (F(p2)))" ... + $ exit_status.deter : chr "ok" "ok" "ok" "ok" ... + $ exit_status.small : chr "ok" "ok" "ok" "ok" ... + $ exit_code.deter : int 0 0 0 0 0 0 0 0 0 0 + $ exit_code.small : int 0 0 0 0 0 0 0 0 0 0 + $ time.deter : num 0.0174 0.0149 0.0141 0.0136 0.0128 ... + $ time.small : num 0.0171 0.0155 0.0152 0.0146 0.0139 ... + $ states.deter : int 31 15 7 3 1 4 8 16 32 2 + $ states.small : int 6 5 4 3 1 4 8 16 32 2 + $ edges.deter : int 211 65 19 5 1 9 27 81 243 3 + $ edges.small : int 10 8 6 5 1 9 27 81 243 3 + $ transitions.deter : int 781 175 37 7 1 16 64 256 1024 4 + $ transitions.small : int 160 64 24 7 1 16 64 256 1024 4 + $ acc.deter : int 1 1 1 1 1 1 1 1 1 1 + $ acc.small : int 1 1 1 1 1 1 1 1 1 1 + $ scc.deter : int 31 15 7 3 1 4 8 16 32 2 + $ scc.small : int 6 5 4 3 1 4 8 16 32 2 + $ nondet_states.deter : int 0 0 0 0 0 0 0 0 0 0 + $ nondet_states.small : int 1 1 1 0 0 0 0 0 0 0 + $ nondet_aut.deter : int 0 0 0 0 0 0 0 0 0 0 + $ nondet_aut.small : int 1 1 1 0 0 0 0 0 0 0 + $ complete_aut.deter : int 0 0 0 0 0 1 1 1 1 1 + $ complete_aut.small : int 0 0 0 0 0 1 1 1 1 1 + $ product_states.deter : int 5130 2527 1387 598 200 798 1587 2727 5330 400 + $ product_states.small : int 1000 801 601 598 200 798 1587 2727 5330 400 + $ product_transitions.deter: int 82897 37226 18792 7367 2055 16533 33068 57786 114068 8272 + $ product_transitions.small: int 10707 8468 6171 7367 2055 16533 33068 57786 114068 8272 + $ product_scc.deter : int 349 73 33 4 2 5 34 74 350 3 + $ product_scc.small : int 6 5 4 4 2 5 34 74 350 3 + - attr(*, ".internal.selfref")= + - attr(*, "sorted")= chr "formula" +#+end_example - - Complemented intersection check. If $P_i$ and $N_i$ are - deterministic, =ltlcross= builds their complements, $Comp(P_i)$ - and $Comp(N_i)$, and then ensures that $Comp(P_i)\otimes - Comp(N_i)$ is empty. If only one of them is deterministic, for - instance $P_i$, we check that $P_j\otimes Comp(P_i)$ for all $j - \ne i$; likewise if it's $N_i$ that is deterministic. +Using the above form, it is easy to compare two tools on some given +measurement, as we just need to plot two columns. For example to +compare the number of states produced by the two configurations of +=ltl2tgba= for each formula, we just need to plot column +=dt2$state.small= against =dt2$state.deter=. - By default this check is only done for deterministic automata, - because complementation is relatively cheap is that case (at least - it is cheap for simple acceptance conditions). Using option - =--determinize=, =ltlcross= can be instructed to perform - complementation of non-deterministic automata as well, ensuring - precise equivalence checks between all automata. However be aware - that this determinization + complementation may generate large - automata. +#+BEGIN_SRC R :session :results output graphics :width 5 :height 5 :file ltlcross-r.svg :exports both +library(ggplot2) +ggplot(dt2, aes(x=states.small, y=states.deter)) + + geom_abline(colour='white') + geom_point() +#+END_SRC - When validating a translator with =ltlcross= without using the - =--determinize= option we highly recommend to include a translator - with good deterministic output to augment test coverage. Using - '=ltl2tgba -lD %f >%O=' will produce deterministic automata for - all obligation properties and many recurrence properties. Using - '=ltl2dstar --ltl2nba=spin:pathto/ltl2tgba@-Ds %L %O=' will - systematically produce a deterministic Rabin automaton (that - =ltlcross= can complement easily). +#+RESULTS: +[[file:ltlcross-r.svg]] - - Cross-comparison checks: for some state-space $S$, - all $P_i\otimes S$ are either all empty, or all non-empty. - Similarly all $N_i\otimes S$ are either all empty, or all non-empty. - A cross-comparison failure could be displayed as: +We should probably print the formulas for the cases where the two +sizes differ. - : error: {P0,P2} disagree with {P1} when evaluating the state-space - : the following word(s) are not accepted by {P1}: - : P0 accepts: p0 & !p1 & !p2 & p3; p0 & p1 & !p2 & p3; p0 & p1 & p2 & p3; cycle{p0 & p1 & p2 & p3; p0 & p1 & !p2 & !p3; p0 & p1 & p2 & !p3; p0 & p1 & !p2 & !p3} - : P2 accepts: p0 & !p1 & !p2 & p3; cycle{p0 & p1 & !p2 & !p3; p0 & p1 & p2 & p3; p0 & p1 & !p2 & p3} +#+BEGIN_SRC R :session :results output graphics :width 5 :height 5 :file ltlcross-r2.svg :exports both +ggplot(dt2, aes(x=states.small, y=states.deter)) + + geom_abline(colour='white') + geom_point() + + geom_text(data=subset(df2, states.small != states.deter), + aes(label=formula), hjust=0, nudge_x=.5) +#+END_SRC - If =--products=N= is used with =N= greater than one, the number of - the state-space is also printed. This number is of no use by - itself, except to explain why you may get multiple disagreement - between the same sets of automata. +#+RESULTS: +[[file:ltlcross-r2.svg]] - These products tests may sometime catch errors that were not - captured by the first two tests if one non-deterministic automaton - recognize less words than what it should. If the input automata - are deterministic or the =--determinize= option is used, this test - is redundant and can be disabled. (In fact, the =--determinize= - option implies option =--product=0= to do so.) - - - Consistency check: - - For each $i$, the products $P_i\otimes S$ and $N_i\otimes S$ - actually cover all states of $S$. Because $S$ does not have any - deadlock, any of its infinite path must be accepted by $P_i$ or - $N_i$ (or both). - - An error in that case is displayed as - - : error: inconsistency between P1 and N1 - - If =--products=N= is used with =N= greater than one, the number of - the state-space in which the inconsistency was detected is also - printed. - - This test may catch errors that were not captured by the first two - tests if one non-deterministic automaton recognize less words than - what it should. If the input automata are deterministic or the - =--determinize= option is used, this test is redundant and can be - disabled. (In fact, the =--determinize= option implies option - =--product=0= to do so.) - -The above checks are similar to those that are performed by [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], -except for the complemented intersection check, which is only done in -=ltlcross=. - -If any problem was reported during the translation of one of the -formulas, =ltlcheck= will exit with an exit status of =1=. Statistics -(if requested) are output nonetheless, and include any faulty -automaton as well. * Miscellaneous options From 1be313ef0b9f16d6fd35149b074a8d166d740a37 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 10 Aug 2018 14:07:35 +0200 Subject: [PATCH 02/23] get rid of the Python-based CGI translator We now have a separate project for its replacement at https://gitlab.lrde.epita.fr/spot/spot-web-app/ * python/ajax/: Remove directory. * python/Makefile.am, configure.ac, README: Adjust. * NEWS: Mention this. --- NEWS | 6 +- README | 1 - configure.ac | 1 - python/Makefile.am | 2 - python/ajax/Makefile.am | 40 -- python/ajax/README | 90 --- python/ajax/css/loading.gif | Bin 4176 -> 0 bytes python/ajax/css/tipTip.css | 114 --- python/ajax/css/trans.css | 129 ---- python/ajax/js/jquery.ba-bbq.min.js | 18 - python/ajax/js/jquery.ba-dotimeout.min.js | 9 - python/ajax/js/jquery.tipTip.minified.js | 21 - python/ajax/protocol.txt | 124 ---- python/ajax/spotcgi.in | 827 ---------------------- python/ajax/trans.html | 754 -------------------- 15 files changed, 5 insertions(+), 2131 deletions(-) delete mode 100644 python/ajax/Makefile.am delete mode 100644 python/ajax/README delete mode 100644 python/ajax/css/loading.gif delete mode 100644 python/ajax/css/tipTip.css delete mode 100644 python/ajax/css/trans.css delete mode 100644 python/ajax/js/jquery.ba-bbq.min.js delete mode 100644 python/ajax/js/jquery.ba-dotimeout.min.js delete mode 100644 python/ajax/js/jquery.tipTip.minified.js delete mode 100644 python/ajax/protocol.txt delete mode 100755 python/ajax/spotcgi.in delete mode 100644 python/ajax/trans.html diff --git a/NEWS b/NEWS index 11a6c17ed..4cd48b3e0 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 2.6.1.dev (not yet released) - Nothing yet. + Build: + + - We no longer distribute the Python-based CGI script + javascript + code for the online translator. Its replacement has its own + repository: https://gitlab.lrde.epita.fr/spot/spot-web-app/ New in spot 2.6.1 (2018-08-04) diff --git a/README b/README index c130e2f98..1c23ac463 100644 --- a/README +++ b/README @@ -228,7 +228,6 @@ bench/ Benchmarks for ... stutter/ ... stutter-invariance checking algorithms, wdba/ ... WDBA minimization (for obligation properties). python/ Python bindings for Spot and BuDDy - ajax/ LTL-to-TGBA translator with web interface, using Javascript. Third party software -------------------- diff --git a/configure.ac b/configure.ac index 5d69ccc8e..2edae69bc 100644 --- a/configure.ac +++ b/configure.ac @@ -244,7 +244,6 @@ AC_CONFIG_FILES([ spot/twaalgos/Makefile spot/twa/Makefile spot/gen/Makefile - python/ajax/Makefile python/Makefile tests/core/defs tests/ltsmin/defs:tests/core/defs.in diff --git a/python/Makefile.am b/python/Makefile.am index a9ba4400b..57d3e75ea 100644 --- a/python/Makefile.am +++ b/python/Makefile.am @@ -20,8 +20,6 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -SUBDIRS = . ajax - AUTOMAKE_OPTIONS = subdir-objects AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_builddir) -I$(top_srcdir) \ diff --git a/python/ajax/Makefile.am b/python/ajax/Makefile.am deleted file mode 100644 index af8852b94..000000000 --- a/python/ajax/Makefile.am +++ /dev/null @@ -1,40 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 2011, 2012, 2015, 2016, 2018 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). -## -## This file is part of Spot, a model checking library. -## -## Spot is free software; you can redistribute it and/or modify it -## under the terms of the GNU General Public License as published by -## the Free Software Foundation; either version 3 of the License, or -## (at your option) any later version. -## -## Spot is distributed in the hope that it will be useful, but WITHOUT -## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -## License for more details. -## -## You should have received a copy of the GNU General Public License -## along with this program. If not, see . - -nodist_noinst_SCRIPTS = spotcgi.py -EXTRA_DIST = $(srcdir)/spotcgi.in README trans.html css/trans.css \ - css/tipTip.css js/jquery.tipTip.minified.js js/jquery.ba-bbq.min.js \ - js/jquery.ba-dotimeout.min.js css/loading.gif protocol.txt - -CLEANFILES = $(nodist_noinst_SCRIPTS) - -spotcgi.py: $(srcdir)/spotcgi.in Makefile - sed -e 's|[@]PYTHON[@]|@PYTHON@|g' \ - -e 's|[@]pythondir[@]|@pythondir@|g' \ - -e 's|[@]srcdir[@]|@srcdir@|g' \ - -e 's|[@]top_builddir[@]|@top_builddir@|g' \ - -e 's|[@]PACKAGE_VERSION[@]|@PACKAGE_VERSION@|g' \ - -e 's|[@]DOT[@]|@DOT@|g' \ - -e 's|[@]LTL3BA[@]|@LTL3BA@|g' \ - <$(srcdir)/spotcgi.in >spotcgi.tmp - chmod +x spotcgi.tmp - mv -f spotcgi.tmp $@ - -clean-local: - rm -rf spotimg diff --git a/python/ajax/README b/python/ajax/README deleted file mode 100644 index 4a9055673..000000000 --- a/python/ajax/README +++ /dev/null @@ -1,90 +0,0 @@ -ltl2tgba.html is a dynamic web page that translates user-supplied LTL -formulae to Transition-based Generalized Büchi Automata. The actual -translation work is performed by a CGI script in Python: spotcgi.py. - -There are two ways to use the script: using a web server such as -Apache, or standalone. - -In both cases you should ensure that the command `dot', from the -GraphViz package, is in the PATH. configure should have picked it up. - -The "ltl3ba" tab will only be enabled if ltl3ba is available (as -checked by ./configure) and supports options -v/-T/-T3 (checked by the -CGI script). These option were introduced into ltl3ba version 1.1.0. - - -Standalone usage -================ - -Simply run spotcgi.py from this directory. This will create a directory -called spotimg/ in the current directory (this will hold the generated -pictures) and start an HTTP server on port 8000. Point your browser -to http://localhost:8000/trans.html and you should be OK. - -After you have killed the server process (e.g. with Control-C), -you may want to erase the spotimg/ directory. - - -Installing on a real web server -=============================== - -1) Install Spot first (run `make install' from the top-level). - - The CGI script uses the Python bindings and assume they - have been installed. Near the top of the script, you - should see a call to sys.path.insert(), with the expected - location of the Python bindings for spot. This path was - configured from ./configure's arguments and you should not - have to fiddle with it. I'm mentionning it just in case. - -2) Copy spotcgi.py to some place were CGI execution is allowed. - Depending on your HTTP server's configuration, you may have - to rename the script as spotcgi.cgi or something else, so - that the server accepts to run it. - - Apache users in trouble should look at the following options - before digging the Apache manual deeper. These can go - in a .htaccess file (if allowed). - - # Treat *.py files as CGI scripts - AddHandler cgi-script .py - - # Allow CGI execution in some directory. - Options +ExecCGI - -3) In the directory where you have installed spotcgi.py, - create a subdirectory called spotimg/. This is where - the script will cache its images and other temporary - files. (If you want to change this name, see the imgdir - variable at the top of the script.) - - This directory must be writable by the Unix user that - will run the script when the HTTP server processes the - request. - - spotcgi.py purges old files at most once every hour. - -4) Copy the directories css/, js/, and logos/ along with trans.html - to their destination. You may have to adjust a few paths at the - top of the html page. - - -Debugging -========= - -When working on the script, remember that the contents of spotimg/ is -used as a cache and that a request will not be processed again if its -result is in the cache. So if you don't understand why the change you -have performed has no effect, make sure you are performing some fresh -query, or wipe the contents of the cache (i.e., erase all files inside -spotimg/ but not the spotimg/ directory itself). - - -The hash string displayed in the web browser is the query string sent -to the CGI script, so you can simulate the call from the command line -with a command like this: - - % export QUERY_STRING="f=a+U+b&r=br&r=lf&r=si&r=eu&o=a&ff=o&mf=d&af=t&ra=t&rf=p&t=fm&fm=od&fm=sm&la=sp&ta=lc&as=ps&ec=Cou99&eo=" - % export SCRIPT_NAME=spotcgi.py - % export SERVER_SOFTWARE=SimpleHTTP - % ./spotcgi.py diff --git a/python/ajax/css/loading.gif b/python/ajax/css/loading.gif deleted file mode 100644 index e15844396f9b8c4d915f5cf595e2a22014a24426..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 4176 zcmZ?wbhEHbRA5kG_{PBS|Nnmm28Lh1em#2h=+dQ2SFT)n_wL=FKYzY``?h1pj+~qv z7Z(>lKfjKSj%(Mhefjd`*s)_iK0YigEOK&k4<0;t_3G8UdGnSnTlVSGr>?FpDJdy4 zGqYX0cHO&o@7AqbRaI3sHZ~d>8ag^UD^{#1D=XvU<5N;nTD59bSXkJbH*eb7+7uKN zczAf$tXU%?BXi=!2{AD-E-o%LHMN$OmP3aQ+1c3%2?>>yluVj5X~KjF5)u+UJw4mD zZ8I=1*t2KPlqpl3oSbglxUpo(k^=`0oH}*t%$YM$QBf)?Dt&!@b#-+`MMVt_4ICUC z`}XZyw{BfcP0h4v(=swLva+(aY}s<>&YgsWgiV_^ZP>7(qN3v5xpPfTO%V|hMn*+Z`i-Cbb2jm7&Br>r7Z(wL@ zZfR|6@96C6?&TAxnc5o|eK(t&eflc>D5&=xg$ zQFeAd8_`x#S^iEYPK7PUq&X)r>}=8WcJt%t;1^RowpHv>JBzd`7h4C1xYBhYMfEA| zqUSGmu(R;!T<38)^-AtwCz~?2l$joPOF~8H3kEiR-H-`49x}@ubmUM-QJC0xn1T7F zjN#)c3QcW74Dox45)Lx8Ix>q)**$T6V5_>Y&zk~|1jn7Mdu0L*oV*>+G4Y%-JaLnQ zd5RRb8xKpuf`cr{dIc#tDGeNg?WbilZX_fzcTVQ#4th|a)X3bE$ZuPbsK~Bg-8sW- zS962YF%|)Pv!kj>jmLsYRT3naja2m7rS!~FoUbst@+2#|X*f4HN(T$6X1FeFTG7;W zW{blQ289J2lT_4;k^&f;JvlX9xXZ3ASbV&PaaYd)jf;nwc9gqiNz63bdZC%c*e>El zfx{f0WH%cQs|O1`8Bcexgshmr-#9^ei5>*E*j)X?zO=kK4{%VgpvB_t%}Ccrdn8H1>|@PY-xo}$ZJ+4xvQ znH=4G)+}&y+}Om<$E(2;;p^hITS#^9egW=&f%O747L~vXR~`ENP=* zu)r+ZdFe_|=9wH$ilp7qMVNL`g3|;g)~0-hJXX!AolTSc zg%S)J9{AkrR_9UD@Mu_=tjxpOCcx>m;F|s976S{zO$@E9(FWYI5<&}ER`9AT9CKng z$i&#iUzecm$TWE~pPQ3L1M36EzNNm_RUJyrE;bD8v%X9@kmSt0aJfK5VB=x9QHe{`Ni=JwRYN0_-v*nihF1rZH=R^eaA=fB+LzoaqgWgu+q2hW z;?FPa>`b^Ltd)Vit+T6>UDP$!k-vL#8#|vjx2c=5=#+U3BL3P!LaGkBli2wsIOg#) zvodoq**W+u5wenJmT(cXQ0HUnmhj_>=CTphjoGm@kVQRONlltdKfZGdx2mcY52vr- zIX!=ILDe04Tp^uoyjDBZEFHDnm*@!kNvfR_;+7E*^_s}SrpGJE6S5(p=(Hon z+ZG<(;Kboq(5cwS$)VoCr*VYg0ppbF9T5y43pWO^igH)EoG^3<6c;gjQu|^7hhwXn zZd-^z2FGDhWm~759ga(;DzZp83B8Rx&?z7%vW)AHgG0vzCS6;_8B5omoF-t@X0$7D!dTH)BJ&mm^wpk$J!KK{h)(!Ku3NpM_F!3q7 z>0CKt{nCMppUvz_If}vyADKfEg@_ z%$mXhN!nfu8QfZwCO73Y20nUxmtCZdPpH6^OXOmgoJHrPN@E5d)-91fgEWy4a zoxM|A`NgB99lTklOq|(Jvk=WA6r05v*AZ9Cv^8~%{0-ciusRz^zWZ8JO zmM}Cm$?5qpI6lf}=+kwJl2G7Uz{Dy3%PfXLA%Ux7I?q-kA=L@~@;s~`bXp`{H0v<7 z^Pgm}a9}>#qRiDafmf)p)lSxvW$A;94D1tE_R2lU$mC*cR%{knV(_7JMY}9_RZd4y zs!pUE`)-SwP7H^$1K7Q^R|P2avDnd$tfR3%^YDSHKWaLBqk&gx|66Bl!tz^*T-Dx}I2%f!aX#S^G3+9?}hYZNH3RMg%fiCavR z!#Ub&A$Qn>c4yP|wqnmkWyE|hNZ1>#7t%Jq(8lg^SV-D$j&KQAL!*rQyPXwA41rwS z8cHTF0yYRR$#HubXfir^=+%jKT#yL37{JQSW9D+hG4NvJq;{5&io{m-Mn;K*Jf@im z$A!3A1VpNK77H|qY4~IaENnQilHElo;^y|v&4NkmeNsFa6Q(m6D(LY{VOe;5Z<3o; zN$UoOCT`J~6XimMrR!Zpw3=*GRvt{~x-ge{QBSoho2MS5Y|S2nfGJ^3S}{%y9zhEp zFfv*R${Gl;IB{#(N3qPjIzxbo$#T(xfP{mN=PtE2B?x}xI>w|}$S?ci!y)f97BMq} zo$6f-na;9yIu1@-Cot+Zzi-@7v`3&(S6F0)?UW?XFX5)kLexVZ9_saJVcElW?&%sn z6cq|3r1 ztg;$m9)z-PS9cGSsH`S?&*UanNiH$bDLouw(oz}%lV*3$RZ`_PSZ&!Uo2!Mn~o{mrNzYz*Zi;LsL7PQUkh#tvR;1q^;MAK^krKL4 zW+k)!qAvoCi;fyPGnPwLF+6nVlXGU}T<{?Ih$xe~IHy2^f-7rF^Q)B+2U4AKBN;l5%wp^&Arc2gmM~43FI1xOlA)A?`I1nW&dj7EE}cR#Ap#pOEdJQSzlFE5 zBB`nK46B&Y35C52SlN~JybdrJDd{P)I4>%gDWJqOMNy?>f>>hW0TE4&o`?k#I1Yc1 zv|P4h*2bnUZDJe=4i4fhF30%TM3)4dW46)R5S|w#VBq1vy)@yVnDmte2Lv*7RXS?J z3obMUcCp}VG=cJPS9cEsdpvvZBnEyKJK2eoyB+;C0z_wZyJ#rNGq>=w@%Q%6Y!Vgo zw~=TT)#cS)(8VNc$Gnb7Q)EjMlQWMR4<|<#n^?5&kq!>O7$Ir#)t&sl)-Go{*;%;+ zRan+_NQmC*;+V$rrj?zEgNgmc?r$&o?80J2n4Dy*3|PEb6g0{z4s3tHz{bPK$e|#V z+RDPI>hk2m)f01DW$YZ5Zn*Gx(Mb*$2_>#3*CP{kWdwMBJUH~kRZk{F%E}<+psS%h zPe?|>p=B%rzDi~)2`=uO0#0%^JA@XtcuH`IZSpcy;_BkzdspfZl+45<$+OHOJEYNL zI^Tl_6>|d`U0Ye@S+z7$OU_?t=3@1$xgo^L-nh4wCFI2dbHOI@z`iLB2VK3}GhNCw zPJG}ETLPb6>z#+9&-72SRLx7^I08>a9=ZA-%A2G=-SmV>$uZcN*m=!)+ai|) zhbCsmS!z2Y3>p?Rw5o~;6wJ*O6*%B1%y(m%OOE(ghE_%fg#bp@UR|XFtrHJiaxPbO lIpA!=7);function a(j){j=j||location.href;return"#"+j.replace(/^[^#]*#?(.*)$/,"$1")}$.fn[c]=function(j){return j?this.bind(c,j):this.trigger(c)};$.fn[c].delay=50;g[c]=$.extend(g[c],{setup:function(){if(d){return false}$(f.start)},teardown:function(){if(d){return false}$(f.stop)}});f=(function(){var j={},p,m=a(),k=function(q){return q},l=k,o=k;j.start=function(){p||n()};j.stop=function(){p&&clearTimeout(p);p=b};function n(){var r=a(),q=o(m);if(r!==m){l(m=r,q);$(e).trigger(c)}else{if(q!==m){location.href=location.href.replace(/#.*/,"")+q}}p=setTimeout(n,$.fn[c].delay)}$.browser.msie&&!d&&(function(){var q,r;j.start=function(){if(!q){r=$.fn[c].src;r=r&&r+a();q=$('