Reading and writing CSV files

All the tools that normally produce formulas (like genltl, randltl, and ltlfilt) have a --format option that can be used to customize the way output is formatted.

For instance here is how we could use genltl to generate a CSV file with three columns: the family name of the formula, its parameter, and the formula itself.

genltl --and-gf=1..5 --u-left=1..5 --format='%F,%L,%f' > gen.csv
cat gen.csv

and-gf,1,GFp1
and-gf,2,GFp1 & GFp2
and-gf,3,GFp1 & GFp2 & GFp3
and-gf,4,GFp1 & GFp2 & GFp3 & GFp4
and-gf,5,GFp1 & GFp2 & GFp3 & GFp4 & GFp5
u-left,1,p1
u-left,2,p1 U p2
u-left,3,(p1 U p2) U p3
u-left,4,((p1 U p2) U p3) U p4
u-left,5,(((p1 U p2) U p3) U p4) U p5

Tools that produce automata (like ltl2tgba, dstar2tgba, autfilt, or randaut) have a --stats option that can be used to output various statistics about the constructed automaton (these statistics are shown instead of printing the automaton, but one of those allows printing the automaton as a one-liner in the HOA format).

For instance, the following command will translate all the previous formulas, and show the resulting number of states (%s) and edges (%e) of the automaton constructed for each formula.

genltl --and-gf=1..5 --u-left=1..5 | ltl2tgba --stats '%f,%s,%e'

GFp1,1,2
G(Fp1 & Fp2),1,4
G(Fp1 & Fp2 & Fp3),1,8
G(Fp1 & Fp2 & Fp3 & Fp4),1,16
G(Fp1 & Fp2 & Fp3 & Fp4 & Fp5),1,32
p1,2,2
p1 U p2,2,3
(p1 U p2) U p3,4,10
((p1 U p2) U p3) U p4,8,34
(((p1 U p2) U p3) U p4) U p5,16,116

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:

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 second line of this input does no conform to RFC 4180 because 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:

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 quotes and automatically double any double quote output between them, as per RFC 4180.

The tool ltlcross has its own --csv=FILENAME option to format the statistics it gathers in a CSV file, but you have very little control hover how this CSV file is formatted (it can only be changed via option such as --products or --omit-missing).

All the tools that read formulas from files extend the filename syntax to support the specification of a CSV column. The notation filename/COL denotes the column COL of that file.

For instance let's consider the file gen.csv built with the first command of this page. It contains:

and-gf,1,GFp1
and-gf,2,GFp1 & GFp2
and-gf,3,GFp1 & GFp2 & GFp3
and-gf,4,GFp1 & GFp2 & GFp3 & GFp4
and-gf,5,GFp1 & GFp2 & GFp3 & GFp4 & GFp5
u-left,1,p1
u-left,2,p1 U p2
u-left,3,(p1 U p2) U p3
u-left,4,((p1 U p2) U p3) U p4
u-left,5,(((p1 U p2) U p3) U p4) U p5

We can run ltl2tgba on the third column to produce the same output as in a previous example:

ltl2tgba -F gen.csv/3 --stats '%f,%s,%e'

GFp1,1,2
G(Fp1 & Fp2),1,4
G(Fp1 & Fp2 & Fp3),1,8
G(Fp1 & Fp2 & Fp3 & Fp4),1,16
G(Fp1 & Fp2 & Fp3 & Fp4 & Fp5),1,32
p1,2,2
p1 U p2,2,3
(p1 U p2) U p3,4,10
((p1 U p2) U p3) U p4,8,34
(((p1 U p2) U p3) U p4) U p5,16,116

When ltlfilt is used on a CSV file, it will preserve the text before and after the matched formula in the CSV file. For instance:

ltlfilt -F gen.csv/3 --size-min=8 --relabel=abc

and-gf,3,GFa & GFb & GFc
and-gf,4,GFa & GFb & GFc & GFd
and-gf,5,GFa & GFb & GFc & GFd & GFe
u-left,5,(((a U b) U c) U d) U e

The preservation in the output of the text before and after the selected column can be altered using the --format option. The %< escape sequence represent the (comma-separated) data of all the columns before the selected column, and %> is the same for the trailing data. Note that the comma that separate formulas' column from the other column are excluded and should be added in the format string.

For instance this moves the first two columns after the formulas.

ltlfilt -F gen.csv/3 --size-min=8 --format='"%f",%<'

"GFp1 & GFp2 & GFp3",and-gf,3
"GFp1 & GFp2 & GFp3 & GFp4",and-gf,4
"GFp1 & GFp2 & GFp3 & GFp4 & GFp5",and-gf,5
"(((p1 U p2) U p3) U p4) U p5",u-left,5

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 uses double quotes, and the input CSV file had more than one column.

Typical uses of ltlfilt on CSV file include:

• Filtering lines based on an LTL criterion, as above.
• Changing the syntax of LTL formulas. For instance ltl2tgba's --stats option, and ltlcross's --csv option always output formulas in Spot's format. If that is inappropriate, simply use ltlfilt to rewrite the relevant column in your preferred syntax.

Some CSV files contain a header lines that should not be processed. For instance the CSV files produced by ltlcross have such a line:

randltl -n 2 a b | ltlfilt --remove-wm |
  ltlcross --csv=results.csv 'ltl2tgba -s %f >%N' 'ltl3ba -f %s >%N'
cat results.csv

"formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nondet_states","nondet_aut","complete_aut","product_states","product_transitions","product_scc"
"0","ltl2tgba -s %f >%N","ok",0,0.0358857,1,1,0,1,1,0,0,0,1,0,1
"0","ltl3ba -f %s >%N","ok",0,0.0079831,1,0,0,1,1,0,0,0,1,0,1
"1","ltl2tgba -s %f >%N","ok",0,0.035928,1,1,1,1,1,0,0,1,200,4199,1
"1","ltl3ba -f %s >%N","ok",0,0.00803175,1,1,1,1,1,0,0,1,200,4199,1
"!(F(!(b)))","ltl2tgba -s %f >%N","ok",0,0.0363511,1,1,1,1,1,0,0,0,200,2059,1
"!(F(!(b)))","ltl3ba -f %s >%N","ok",0,0.0088513,1,1,1,1,1,0,0,0,200,2059,1
"F(!(b))","ltl2tgba -s %f >%N","ok",0,0.0361925,2,3,4,1,2,0,0,1,400,8264,2
"F(!(b))","ltl3ba -f %s >%N","ok",0,0.00797494,2,3,4,1,2,0,0,1,400,8264,2

If we run ltlfilt on the first column, it will process the formula header as if it was an LTL formula.

ltlfilt -F results.csv/1 --format='%f' --unique

formula
0
1
!F!b
F!b

In such case, the syntax FILENAME/-COL (with a minus sign before the column number) can be used to discard the first line of a CSV file.

ltlfilt -F results.csv/-1 --format='%f' --unique

0
1
!F!b
F!b

The --stats option of tools that generate automata can be used to generate CSV files that embed automata. For instance

genltl --dac=1..3 | ltl2tgba --stats='"%f","%e edges","%h"' > csv-aut.csv
cat csv-aut.csv

"G!p0","1 edges","HOA: v1 name: ""G!p0"" States: 1 Start: 0 AP: 1 ""p0"" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic stutter-invariant very-weak --BODY-- State: 0 [!0] 0 --END--"
"(!p1 U p0) | G!p0","5 edges","HOA: v1 name: ""(!p1 U p0) | G!p0"" States: 3 Start: 2 AP: 2 ""p1"" ""p0"" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic stutter-invariant very-weak --BODY-- State: 0 [!1] 0 State: 1 [t] 1 State: 2 [0&!1] 0 [1] 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: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic stutter-invariant very-weak --BODY-- State: 0 [!1] 0 State: 1 [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.

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 %< and %> in the --stats format.

autfilt csv-aut.csv/3 --states=2..3 --stats='%<,"%h"'

"(!p1 U p0) | G!p0","5 edges","HOA: v1 States: 3 Start: 2 AP: 2 ""p1"" ""p0"" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic stutter-invariant very-weak --BODY-- State: 0 [!1] 0 State: 1 [t] 1 State: 2 [0&!1] 0 [1] 1 [!0&!1] 2 --END--"
"G(!p0 | G!p1)","3 edges","HOA: v1 States: 2 Start: 1 AP: 2 ""p0"" ""p1"" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic stutter-invariant very-weak --BODY-- State: 0 [!1] 0 State: 1 [0&!1] 0 [!0] 1 --END--"

Another source of automata in CSV format is ltlcross. Using options --automata it will record the automata produced by each tool into the CSV file:

genltl --dac=1..3 | ltlcross --csv=result.csv --automata ltl2tgba
cat result.csv

"formula","tool","exit_status","exit_code","time","states","edges","transitions","acc","scc","nondet_states","nondet_aut","complete_aut","product_states","product_transitions","product_scc","automaton"
"G(!(p0))","ltl2tgba","ok",0,0.0364722,1,1,1,0,1,0,0,0,200,2055,2,"HOA: v1 name: ""G!p0"" States: 1 Start: 0 AP: 1 ""p0"" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic stutter-invariant very-weak --BODY-- State: 0 [!0] 0 --END--"
"!(G(!(p0)))","ltl2tgba","ok",0,0.0359809,2,3,4,1,2,0,0,1,400,8272,3,"HOA: v1 name: ""Fp0"" States: 2 Start: 1 AP: 1 ""p0"" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete deterministic stutter-invariant terminal very-weak --BODY-- State: 0 {0} [t] 0 State: 1 [0] 0 [!0] 1 --END--"
"(F(p0)) -> ((!(p1)) U (p0))","ltl2tgba","ok",0,0.0372907,3,5,10,0,3,0,0,0,598,10379,4,"HOA: v1 name: ""(!p1 U p0) | G!p0"" States: 3 Start: 2 AP: 2 ""p1"" ""p0"" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic stutter-invariant very-weak --BODY-- State: 0 [!1] 0 State: 1 [t] 1 State: 2 [0&!1] 0 [1] 1 [!0&!1] 2 --END--"
"!((F(p0)) -> ((!(p1)) U (p0)))","ltl2tgba","ok",0,0.0368437,3,5,10,1,3,0,0,0,598,10398,4,"HOA: v1 name: ""Fp0 & (p1 R !p0)"" States: 3 Start: 1 AP: 2 ""p1"" ""p0"" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc deterministic stutter-invariant very-weak --BODY-- State: 0 {0} [t] 0 State: 1 [!0&!1] 1 [0&!1] 2 State: 2 [1] 0 [!1] 2 --END--"
"G((p0) -> (G(!(p1))))","ltl2tgba","ok",0,0.0424382,2,3,5,0,2,0,0,0,400,5025,2,"HOA: v1 name: ""G(!p0 | G!p1)"" States: 2 Start: 1 AP: 2 ""p0"" ""p1"" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic stutter-invariant very-weak --BODY-- State: 0 [!1] 0 State: 1 [0&!1] 0 [!0] 1 --END--"
"!(G((p0) -> (G(!(p1)))))","ltl2tgba","ok",0,0.0375193,3,6,12,1,3,0,0,1,600,12354,3,"HOA: v1 name: ""F(p0 & Fp1)"" States: 3 Start: 2 AP: 2 ""p0"" ""p1"" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete deterministic stutter-invariant terminal very-weak --BODY-- State: 0 {0} [t] 0 State: 1 [1] 0 [!1] 1 State: 2 [0&1] 0 [0&!1] 1 [!0] 2 --END--"