Commit ed361bb0 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

org: add remark about "%h"

* doc/org/csv.org: Mention that %h must be double-quoted in CSV output.
parent f58f61b3
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment