diff --git a/doc/org/csv.org b/doc/org/csv.org index 122d277dd..75bb7a2a8 100644 --- a/doc/org/csv.org +++ b/doc/org/csv.org @@ -62,7 +62,7 @@ p1 U p2,2,3 (((p1 U p2) U p3) U p4) U p5,16,116 #+end_example -If the translated formulas may contain commas, or double-quotes, this +If the translated formulas may contain commas, or double quotes, this simple output may prove difficult to process by other tools. For instance consider the translation of the following two formulas: @@ -74,7 +74,7 @@ ltl2tgba -f Xa -f 'G("switch == on" -> F"tab[3,5] < 12")' --stats '%f,%s,%e' : G(!"switch == on" | F"tab[3,5] < 12"),2,4 The second line of this input does no conform to [[https://www.rfc-editor.org/rfc/rfc4180.txt][RFC 4180]] because -non-escaped fields are not allowed to contain comma or double-quotes. +non-escaped fields are not allowed to contain comma or double quotes. To fix this, simply double-quote the =%f= in the argument to =--stats=: #+BEGIN_SRC sh :results verbatim :exports both @@ -85,7 +85,7 @@ ltl2tgba -f Xa -f 'G("switch == on" -> F"tab[3,5] < 12")' --stats '"%f",%s,%e' : "Xa",3,3 : "G(!""switch == on"" | F""tab[3,5] < 12"")",2,4 -The formater will detect your double-quote and automatically double +The formater will detect your double quotes and automatically double any double quote output between them, as per [[https://www.rfc-editor.org/rfc/rfc4180.txt][RFC 4180]]. The tool [[file:ltlcross.org][=ltlcross=]] has its own =--csv=FILENAME= option to format the @@ -175,7 +175,7 @@ Note that if the =--format= option is not specified, the default format is one of: =%f=, =%<,%f=, =%f,%>=, or =%<,%f,%>= depending on whether the input CSV had column before and after the selected one. Furthermore, the formula field is automatically double-quoted if the -formula actually use double-quotes, and the input CSV file had more +formula actually use double quotes, and the input CSV file had more than one column. Typical uses of =ltlfilt= on CSV file include: @@ -233,7 +233,6 @@ ltlfilt -F results.csv/-1 --format='%f' --unique : !G(Fb | F!(b | Gb)) : G(Fb | F!(b | Gb)) - * CSV files containing automata The =--stats= option of tools that generate automata can be used to @@ -249,6 +248,11 @@ cat csv-aut.csv : "G!p0 | (!p1 U p0)","5 edges","HOA: v1 name: ""G!p0 | (!p1 U p0)"" States: 3 Start: 2 AP: 2 ""p0"" ""p1"" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc colored deterministic stutter-invariant weak --BODY-- State: 0 {0} [!0] 0 State: 1 {0} [t] 1 State: 2 {0} [!0&1] 0 [0] 1 [!0&!1] 2 --END--" : "G(!p0 | G!p1)","3 edges","HOA: v1 name: ""G(!p0 | G!p1)"" States: 2 Start: 1 AP: 2 ""p0"" ""p1"" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc colored deterministic stutter-invariant weak --BODY-- State: 0 {0} [!1] 0 State: 1 {0} [0&!1] 0 [!0] 1 --END--" +Note that when producing CSV files, it is important to surround =%h= +with double quotes to indicate that double quotes from the HOA format +(output by =%h=) should be escaped. Otherwise the result would not be +a valid CSV file. + [[file:autfilt.org][=autfilt=]] can process a column of such a CSV file using the same syntax we used previously, but by default it will just output the automata. If you want to preserve the entire line, you should use