Skip to content

Commit 7debb97

Browse files
lemmylemmy
committed
Add Unix-specific tests and update build configuration for test execution
- Introduced `AllTestsUnix.tla` for Unix-only tests that rely on Unix shell commands. - Updated `build.xml` to conditionally run Unix tests on non-Windows systems. - Added `IOUtilsUnixTests.tla` to cover various IOUtils functionalities in a Unix environment, including handling of environment variables and command execution. [CI][Tests] Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
1 parent 6bac6bc commit 7debb97

4 files changed

Lines changed: 150 additions & 131 deletions

File tree

‎build.xml‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,12 @@
103103
</target>
104104

105105
<target name="test" depends="dist" description="Run the modules in tests/ on the TLA+ modules in dist/">
106+
<!-- On Unix, run AllTestsUnix which includes IOExec/shell tests; on Windows, run AllTests only. -->
107+
<condition property="allTests" value="${basedir}/tests/AllTestsUnix">
108+
<not><os family="windows"/></not>
109+
</condition>
110+
<property name="allTests" value="${basedir}/tests/AllTests"/>
111+
106112
<!-- If an assert fails, TLC will return a non-zero exit value which is makes the ant target fail. -->
107113
<java classname="tlc2.TLC" fork="true" failonerror="true">
108114
<!-- Tell Java to use a garbage collector which makes TLC happy. -->
@@ -121,7 +127,9 @@
121127
<arg value="-metadir"/>
122128
<arg value="${basedir}/build/states"/>
123129
<arg value="-cleanup"/>
124-
<arg value="${basedir}/tests/AllTests"/>
130+
<arg value="-config"/>
131+
<arg value="${basedir}/tests/AllTests.cfg"/>
132+
<arg value="${allTests}"/>
125133

126134
<classpath>
127135
<pathelement location="${tlc}/tla2tools.jar" />

‎tests/AllTestsUnix.tla‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
---------- MODULE AllTestsUnix -----------
2+
3+
(***************************************************)
4+
(* Unix-only tests that depend on /bin/sh, bash, *)
5+
(* cat, ls, echo, and Unix path conventions. *)
6+
(***************************************************)
7+
EXTENDS AllTests, IOUtilsUnixTests
8+
9+
===========================================

‎tests/IOUtilsTests.tla‎

Lines changed: 7 additions & 130 deletions
Original file line numberDiff line numberDiff line change
@@ -3,76 +3,10 @@ EXTENDS IOUtils, TLC, TLCExt, Integers
33

44
ASSUME PrintT("IOUtilsTests!A")
55

6-
\* Spaces and quotes should be passed directly to the program.
7-
ASSUME(LET ret == IOExec(<<"echo", "'foo' ", " \"bar\"">>) IN /\ ret.exitValue = 0
8-
/\ ret.stdout = "'foo' \"bar\"\n"
9-
/\ ret.stderr = "")
10-
\* Exit values and standard error should be returned properly.
11-
ASSUME(LET ret == IOExec(<<"cat", "/does/not/exist">>) IN /\ ret.exitValue = 1
12-
/\ ret.stdout = ""
13-
/\ ret.stderr = "cat: /does/not/exist: No such file or directory\n")
14-
15-
\* Spaces and quotes should be passed directly to the program.
16-
ASSUME(LET ret == IOExecTemplate(<<"bash", "-c", "echo %1$s %2$s">>, <<"foo", "bar">>)
17-
IN /\ ret.exitValue = 0
18-
/\ ret.stdout = "foo bar\n"
19-
/\ ret.stderr = "")
20-
21-
\* Spaces and quotes should be passed directly to the program.
22-
ASSUME(LET ret == IOExecTemplate(<<"echo", "'%1$s'", "\"%2$s\"">>, <<" foo", "bar ">>)
23-
IN /\ ret.exitValue = 0
24-
/\ ret.stdout = "' foo' \"bar \"\n"
25-
/\ ret.stderr = "")
26-
27-
\* Exit values and standard error should be returned properly.
28-
ASSUME(LET ret == IOExecTemplate(<<"cat", "/does/not/exist">>, <<>>)
29-
IN /\ ret.exitValue = 1
30-
/\ ret.stdout = ""
31-
/\ ret.stderr = "cat: /does/not/exist: No such file or directory\n")
32-
33-
---------------------------------------------------------------------------------------------------------------------------
34-
35-
ASSUME PrintT("IOUtilsTests!B")
36-
37-
(***********************************************************************)
38-
(* Check that environment variables work with IOUtils!IOExec operator: *)
39-
(***********************************************************************)
40-
416
\* SOME_TEST_ENV_VAR is set in Ant's build.xml file.
42-
43-
ASSUME(LET ret == IOExec(<<"/bin/sh", "-c", "echo $SOME_TEST_ENV_VAR">>)
44-
IN /\ ret.exitValue = 0
45-
/\ ret.stdout = "TLCFTW\n"
46-
/\ ret.stderr = "")
47-
48-
ASSUME(LET ret == IOEnvExec([SOME_VAR_42 |-> "42"], <<"/bin/sh", "-c", "echo $SOME_VAR_42">>)
49-
IN /\ ret.exitValue = 0
50-
/\ ret.stdout = "42\n"
51-
/\ ret.stderr = "")
52-
53-
ASSUME(LET ret == IOEnvExecTemplate([SOME_VAR_42 |-> "42"], <<"/bin/sh", "-c", "echo $SOME_VAR_42">>, <<>>)
54-
IN /\ ret.exitValue = 0
55-
/\ ret.stdout = "42\n"
56-
/\ ret.stderr = "")
57-
58-
ASSUME(LET ret == IOEnvExecTemplate([SOME_VAR_42 |-> "42"], <<"/bin/sh", "-c", "echo $SOME_VAR_42">>, <<>>)
59-
IN /\ ret.exitValue = 0
60-
/\ ret.stdout = "42\n"
61-
/\ ret.stderr = "")
62-
63-
ASSUME(LET ret == IOEnvExecTemplate([A |-> 1, B |-> 2], <<"/bin/sh", "-c", "echo $A $B">>, <<>>)
64-
IN /\ ret.exitValue = 0
65-
/\ ret.stdout = "1 2\n"
66-
/\ ret.stderr = "")
67-
68-
ASSUME(LET ret == IOEnvExec(IOEnv, <<"/bin/sh", "-c", "echo $SOME_TEST_ENV_VAR">>)
69-
IN /\ ret.exitValue = 0
70-
/\ ret.stdout = "TLCFTW\n"
71-
/\ ret.stderr = "")
72-
73-
\* Contrary to the /bin/sh -c echo $SOME_VAR technique above, the IOEnv operator does *not* append a dangling
74-
\* newline to the value. Environment variable names made out of non-legal chars for TLA+ records can fall
75-
\* back to ordinary function application.
7+
\* The IOEnv operator does *not* append a dangling newline to the value (contrary to
8+
\* reading env vars via /bin/sh -c echo). Environment variable names made out of
9+
\* non-legal chars for TLA+ records can fall back to ordinary function application.
7610

7711
ASSUME(IOEnv.SOME_TEST_ENV_VAR = "TLCFTW")
7812
ASSUME(IOEnv["SOME_TEST_ENV_VAR"] = "TLCFTW")
@@ -109,68 +43,11 @@ ASSUME(AssertEq(zeroPadN(0, 1), "0"))
10943

11044
---------------------------------------------------------------------------------------------------------------------------
11145

112-
ASSUME PrintT("IOUtilsTests!C")
113-
114-
(***********************************************************************)
115-
(* Check that TLC can be launched through the IOUtils!IOExec operator: *)
116-
(***********************************************************************)
117-
118-
\* Exit if tlc/tla2tools.jar doesn't exist. Since the tests are run with this tla2tools.jar, this assumption should hold.
119-
ASSUME(LET ret == IOExec(<<"ls", "tlc/tla2tools.jar">>)
120-
IN /\ ret.exitValue = 0
121-
/\ ret.stdout = "tlc/tla2tools.jar\n"
122-
/\ ret.stderr = "")
123-
124-
ASSUME PrintT("IOUtilsTests!C!b")
125-
126-
\* Run TLC without any parameters. TLC prints its version number, git commit, ... to stdout and sets RETVAL ($?) to 1.
127-
ASSUME(LET ret == IOExec(<<"java", "-jar", "tlc/tla2tools.jar">>)
128-
IN /\ PrintT(ret)
129-
/\ ret.exitValue = 1
130-
/\ ret.stderr = "")
131-
132-
ASSUME PrintT("IOUtilsTests!C!c")
133-
134-
\* Run TLC with some basic spec that passes.
135-
ASSUME(LET ret == IOExec(<<"java", "-jar", "tlc/tla2tools.jar", "tests/nested/Counter">>)
136-
IN /\ PrintT(ret)
137-
/\ ret.exitValue = 0
138-
/\ ret.stderr = "")
139-
140-
ASSUME PrintT("IOUtilsTests!C!d")
141-
142-
\* Run TLC with some spec depending on CommunityModules and CM on the classpath.
143-
\* Pass an environment variable to the nested spec.
144-
ASSUME(LET ret == IOEnvExec([SOME_NESTED_VAR |-> "SOME_VAL", B |-> "23"],
145-
<<"java", "-cp", "modules:build/deps:build/modules:tlc/tla2tools.jar", "tlc2.TLC",
146-
"-config", "Counter.cfg", "tests/nested/CounterCM">>)
147-
IN /\ PrintT(ret)
148-
/\ ret.exitValue = 0
149-
/\ ret.stderr = "")
150-
151-
---------------------------------------------------------------------------------------------------------------------------
152-
153-
ASSUME PrintT("IOUtilsTests!D")
154-
155-
ASSUME PrintT("IOUtilsTests!D!A")
156-
157-
file == "/tmp/txt-serialize-test.txt"
158-
payloadTXT == "Some text with \" escapes \" \\"
159-
160-
TXTSerializeResult == Serialize(payloadTXT, file, [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>])
161-
ASSUME(LET ret == TXTSerializeResult IN /\ ret.exitValue = 0
162-
/\ ret.stderr = "")
163-
164-
TXTDeserializeResult == Deserialize(file, [format |-> "TXT", charset |-> "UTF-8"])
165-
ASSUME(LET ret == TXTDeserializeResult IN /\ ret.exitValue = 0
166-
/\ ret.stdout = payloadTXT
167-
/\ ret.stderr = "")
168-
169-
---------------------------------------------------------------------------------------------------------------------------
46+
ASSUME PrintT("IOUtilsTests!B")
17047

17148
\* Simple round-trip test with a variety of different small structures
17249

173-
file2 == "/tmp/bin-serialize-test.vos"
50+
file == "build/tests/bin-serialize-test.vos"
17451
payloadBIN == <<
17552
"foo",
17653
{"bar"},
@@ -179,8 +56,8 @@ payloadBIN == <<
17956
[x |-> 1, y |-> 2]
18057
>>
18158

182-
ASSUME /\ IOSerialize(payloadBIN, file2, FALSE)
183-
/\ LET value == IODeserialize(file2, FALSE)
59+
ASSUME /\ IOSerialize(payloadBIN, file, FALSE)
60+
/\ LET value == IODeserialize(file, FALSE)
18461
IN value = payloadBIN
18562

18663
\* Test: can we read a string TLC has never encountered before?

‎tests/IOUtilsUnixTests.tla‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
-------------------------- MODULE IOUtilsUnixTests --------------------------
2+
EXTENDS IOUtils, TLC, TLCExt, Integers
3+
4+
ASSUME PrintT("IOUtilsUnixTests!A")
5+
6+
\* Spaces and quotes should be passed directly to the program.
7+
ASSUME(LET ret == IOExec(<<"echo", "'foo' ", " \"bar\"">>) IN /\ ret.exitValue = 0
8+
/\ ret.stdout = "'foo' \"bar\"\n"
9+
/\ ret.stderr = "")
10+
\* Exit values and standard error should be returned properly.
11+
ASSUME(LET ret == IOExec(<<"cat", "/does/not/exist">>) IN /\ ret.exitValue = 1
12+
/\ ret.stdout = ""
13+
/\ ret.stderr = "cat: /does/not/exist: No such file or directory\n")
14+
15+
\* Spaces and quotes should be passed directly to the program.
16+
ASSUME(LET ret == IOExecTemplate(<<"bash", "-c", "echo %1$s %2$s">>, <<"foo", "bar">>)
17+
IN /\ ret.exitValue = 0
18+
/\ ret.stdout = "foo bar\n"
19+
/\ ret.stderr = "")
20+
21+
\* Spaces and quotes should be passed directly to the program.
22+
ASSUME(LET ret == IOExecTemplate(<<"echo", "'%1$s'", "\"%2$s\"">>, <<" foo", "bar ">>)
23+
IN /\ ret.exitValue = 0
24+
/\ ret.stdout = "' foo' \"bar \"\n"
25+
/\ ret.stderr = "")
26+
27+
\* Exit values and standard error should be returned properly.
28+
ASSUME(LET ret == IOExecTemplate(<<"cat", "/does/not/exist">>, <<>>)
29+
IN /\ ret.exitValue = 1
30+
/\ ret.stdout = ""
31+
/\ ret.stderr = "cat: /does/not/exist: No such file or directory\n")
32+
33+
---------------------------------------------------------------------------------------------------------------------------
34+
35+
ASSUME PrintT("IOUtilsUnixTests!B")
36+
37+
(***********************************************************************)
38+
(* Check that environment variables work with IOUtils!IOExec operator: *)
39+
(***********************************************************************)
40+
41+
\* SOME_TEST_ENV_VAR is set in Ant's build.xml file.
42+
43+
ASSUME(LET ret == IOExec(<<"/bin/sh", "-c", "echo $SOME_TEST_ENV_VAR">>)
44+
IN /\ ret.exitValue = 0
45+
/\ ret.stdout = "TLCFTW\n"
46+
/\ ret.stderr = "")
47+
48+
ASSUME(LET ret == IOEnvExec([SOME_VAR_42 |-> "42"], <<"/bin/sh", "-c", "echo $SOME_VAR_42">>)
49+
IN /\ ret.exitValue = 0
50+
/\ ret.stdout = "42\n"
51+
/\ ret.stderr = "")
52+
53+
ASSUME(LET ret == IOEnvExecTemplate([SOME_VAR_42 |-> "42"], <<"/bin/sh", "-c", "echo $SOME_VAR_42">>, <<>>)
54+
IN /\ ret.exitValue = 0
55+
/\ ret.stdout = "42\n"
56+
/\ ret.stderr = "")
57+
58+
ASSUME(LET ret == IOEnvExecTemplate([A |-> 1, B |-> 2], <<"/bin/sh", "-c", "echo $A $B">>, <<>>)
59+
IN /\ ret.exitValue = 0
60+
/\ ret.stdout = "1 2\n"
61+
/\ ret.stderr = "")
62+
63+
ASSUME(LET ret == IOEnvExec(IOEnv, <<"/bin/sh", "-c", "echo $SOME_TEST_ENV_VAR">>)
64+
IN /\ ret.exitValue = 0
65+
/\ ret.stdout = "TLCFTW\n"
66+
/\ ret.stderr = "")
67+
68+
---------------------------------------------------------------------------------------------------------------------------
69+
70+
ASSUME PrintT("IOUtilsUnixTests!C")
71+
72+
(***********************************************************************)
73+
(* Check that TLC can be launched through the IOUtils!IOExec operator: *)
74+
(***********************************************************************)
75+
76+
\* Exit if tlc/tla2tools.jar doesn't exist. Since the tests are run with this tla2tools.jar, this assumption should hold.
77+
ASSUME(LET ret == IOExec(<<"ls", "tlc/tla2tools.jar">>)
78+
IN /\ ret.exitValue = 0
79+
/\ ret.stdout = "tlc/tla2tools.jar\n"
80+
/\ ret.stderr = "")
81+
82+
ASSUME PrintT("IOUtilsUnixTests!C!b")
83+
84+
\* Run TLC without any parameters. TLC prints its version number, git commit, ... to stdout and sets RETVAL ($?) to 1.
85+
ASSUME(LET ret == IOExec(<<"java", "-jar", "tlc/tla2tools.jar">>)
86+
IN /\ PrintT(ret)
87+
/\ ret.exitValue = 1
88+
/\ ret.stderr = "")
89+
90+
ASSUME PrintT("IOUtilsUnixTests!C!c")
91+
92+
\* Run TLC with some basic spec that passes.
93+
ASSUME(LET ret == IOExec(<<"java", "-jar", "tlc/tla2tools.jar", "tests/nested/Counter">>)
94+
IN /\ PrintT(ret)
95+
/\ ret.exitValue = 0
96+
/\ ret.stderr = "")
97+
98+
ASSUME PrintT("IOUtilsUnixTests!C!d")
99+
100+
\* Run TLC with some spec depending on CommunityModules and CM on the classpath.
101+
\* Pass an environment variable to the nested spec.
102+
ASSUME(LET ret == IOEnvExec([SOME_NESTED_VAR |-> "SOME_VAL", B |-> "23"],
103+
<<"java", "-cp", "modules:build/deps:build/modules:tlc/tla2tools.jar", "tlc2.TLC",
104+
"-config", "Counter.cfg", "tests/nested/CounterCM">>)
105+
IN /\ PrintT(ret)
106+
/\ ret.exitValue = 0
107+
/\ ret.stderr = "")
108+
109+
---------------------------------------------------------------------------------------------------------------------------
110+
111+
ASSUME PrintT("IOUtilsUnixTests!D")
112+
113+
txtFile == "/tmp/txt-serialize-test.txt"
114+
payloadTXT == "Some text with \" escapes \" \\"
115+
116+
TXTSerializeResult == Serialize(payloadTXT, txtFile, [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>])
117+
ASSUME(LET ret == TXTSerializeResult IN /\ ret.exitValue = 0
118+
/\ ret.stderr = "")
119+
120+
TXTDeserializeResult == Deserialize(txtFile, [format |-> "TXT", charset |-> "UTF-8"])
121+
ASSUME(LET ret == TXTDeserializeResult IN /\ ret.exitValue = 0
122+
/\ ret.stdout = payloadTXT
123+
/\ ret.stderr = "")
124+
125+
=============================================================================

0 commit comments

Comments
 (0)