Skip to content

Commit 70601cc

Browse files
afonsonflemmy
afonsonf
authored and
lemmy
committed
Add text writer and reader using the new serializer interface.
Depends on a version of TLC until after October 2021. Part of Github issue #53 #53 [Feature]
1 parent 0f53203 commit 70601cc

File tree

3 files changed

+167
-2
lines changed

3 files changed

+167
-2
lines changed

‎modules/IOUtils.tla‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,25 @@ IOSerialize(val, absoluteFilename, compress) == TRUE
1010

1111
IODeserialize(absoluteFilename, compressed) == CHOOSE val : TRUE
1212

13+
Serialize(value, dest, options) ==
14+
(*******************************************************************************)
15+
(* value: TLA+ value to be serialized. *)
16+
(* dest: Destination to serialize to such as a file or URL. *)
17+
(* options: Record of serializer-specific options with format mandatory to *)
18+
(* identify a serializer. Read a seriazlier's documentation for serializer- *)
19+
(* specific options. *)
20+
(*******************************************************************************)
21+
CHOOSE r \in [exitValue : Int, stdout : STRING, stderr : STRING] : TRUE
22+
23+
Deserialize(src, options) ==
24+
(*******************************************************************************)
25+
(* src: Destination to serialize to such as a file or URL. *)
26+
(* options: Record of serializer-specific options with format mandatory to *)
27+
(* identify a serializer. Read a seriazlier's documentation for serializer- *)
28+
(* specific options. *)
29+
(*******************************************************************************)
30+
CHOOSE val : TRUE
31+
1332
----------------------------------------------------------------------------
1433

1534
IOExec(command) ==

‎modules/tlc2/overrides/IOUtils.java‎

Lines changed: 129 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,14 +29,24 @@
2929
import java.io.File;
3030
import java.io.IOException;
3131
import java.io.InputStream;
32+
import java.nio.charset.Charset;
33+
import java.nio.file.Files;
34+
import java.nio.file.Paths;
35+
import java.nio.file.StandardOpenOption;
3236
import java.util.ArrayList;
3337
import java.util.Arrays;
3438
import java.util.HashMap;
3539
import java.util.List;
3640
import java.util.Map;
3741

42+
import tla2sany.semantic.ExprOrOpArgNode;
3843
import tlc2.output.EC;
44+
import tlc2.tool.EvalControl;
3945
import tlc2.tool.EvalException;
46+
import tlc2.tool.TLCState;
47+
import tlc2.tool.coverage.CostModel;
48+
import tlc2.tool.impl.Tool;
49+
import tlc2.util.Context;
4050
import tlc2.value.IValue;
4151
import tlc2.value.ValueInputStream;
4252
import tlc2.value.ValueOutputStream;
@@ -52,7 +62,7 @@
5262
public class IOUtils {
5363

5464
@TLAPlusOperator(identifier = "IODeserialize", module = "IOUtils", warn = false)
55-
public static final IValue deserialize(final StringValue absolutePath, final BoolValue compress)
65+
public static final IValue ioDeserialize(final StringValue absolutePath, final BoolValue compress)
5666
throws IOException {
5767
final ValueInputStream vis = new ValueInputStream(new File(absolutePath.val.toString()), compress.val);
5868
try {
@@ -63,7 +73,7 @@ public static final IValue deserialize(final StringValue absolutePath, final Boo
6373
}
6474

6575
@TLAPlusOperator(identifier = "IOSerialize", module = "IOUtils", warn = false)
66-
public static final IValue serialize(final IValue value, final StringValue absolutePath, final BoolValue compress)
76+
public static final IValue ioSerialize(final IValue value, final StringValue absolutePath, final BoolValue compress)
6777
throws IOException {
6878
final ValueOutputStream vos = new ValueOutputStream(new File(absolutePath.val.toString()), compress.val);
6979
try {
@@ -74,6 +84,123 @@ public static final IValue serialize(final IValue value, final StringValue absol
7484
return BoolValue.ValTrue;
7585
}
7686

87+
/* Writes a String as plain text to a file.
88+
* Operator should be called as Serialize(payload, filepath, [format |-> "TXT", charset |-> charset, openOptions |-> openOptions])
89+
* String payload: is the string that will be written
90+
* String filepath: is the file where the string will be written
91+
* String charset: string with a java standard charset
92+
* String openOptions: sequence of strings of java StandardOpenOptions
93+
*
94+
* Example:
95+
* Serialize("test payload", "test.txt", [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITEA", "CREATE", "TRUNCATE_EXISTING">>])
96+
*/
97+
@Evaluation(definition = "Serialize", module = "IOUtils", warn = false, silent = true, priority = 50)
98+
public synchronized static Value textSerialize(final Tool tool, final ExprOrOpArgNode[] args, final Context c,
99+
final TLCState s0, final TLCState s1, final int control, final CostModel cm) {
100+
101+
final String msgInvalidParam = "Serialize error invalid parameters: ";
102+
final String successmsg = "Finish writting to the file with success!";
103+
104+
final RecordValue opts;
105+
106+
try {
107+
opts = (RecordValue) tool.eval(args[2], c, s0, s1, control, cm);
108+
} catch (Exception e){
109+
return new RecordValue(EXEC_NAMES, new Value[] { IntValue.ValOne, new StringValue(""), new StringValue(msgInvalidParam + e.toString()) }, false);
110+
}
111+
112+
final StringValue serializer = (StringValue) opts.apply(new StringValue("format"), EvalControl.Clear);
113+
if("TXT".equals(serializer.getVal().toString())) {
114+
115+
final StringValue payload;
116+
final StringValue filepath;
117+
final StringValue[] openOptions;
118+
final StringValue charset;
119+
120+
try {
121+
payload = (StringValue) tool.eval(args[0], c, s0, s1, control, cm);
122+
filepath = (StringValue) tool.eval(args[1], c, s0, s1, control, cm);
123+
final TupleValue openOptionstv = (TupleValue) opts.apply(new StringValue("openOptions"), EvalControl.Clear);
124+
charset = (StringValue) opts.apply(new StringValue("charset"), EvalControl.Clear);
125+
126+
openOptions = Arrays.asList(openOptionstv.getElems()).stream()
127+
.map(e -> (StringValue) e)
128+
.toArray(size -> new StringValue[size]);
129+
} catch(Exception e) {
130+
return new RecordValue(EXEC_NAMES, new Value[] { IntValue.ValOne, new StringValue(""), new StringValue(msgInvalidParam + e.toString()) }, false);
131+
}
132+
133+
try {
134+
Files.writeString(
135+
Paths.get(filepath.getVal().toString()),
136+
payload.getVal().toString(),
137+
Charset.forName(charset.getVal().toString()),
138+
Arrays.asList(openOptions).stream()
139+
.map(e -> StandardOpenOption.valueOf(e.getVal().toString()) )
140+
.toArray(size -> new StandardOpenOption[size]));
141+
142+
return new RecordValue(EXEC_NAMES, new Value[] { IntValue.ValZero, new StringValue(successmsg), new StringValue("") }, false);
143+
144+
} catch(Exception e) {
145+
final StringValue errormsg = new StringValue("Serialize error writting to the file: "+e.toString());
146+
return new RecordValue(EXEC_NAMES, new Value[] { IntValue.ValOne, new StringValue(""), errormsg }, false);
147+
}
148+
}
149+
150+
return null;
151+
}
152+
153+
/* Reads a String from a plain text file.
154+
* Operator should be called as Deserialize(filepath, [format |-> "TXT", charset |-> charset])
155+
* String filepath: is the file to be read
156+
* String charset: string with a java standard charset
157+
*
158+
* Example:
159+
* Deserialize("test.txt", [format |-> "TXT", charset |-> "UTF-8"])
160+
*/
161+
@Evaluation(definition = "Deserialize", module = "IOUtils", warn = false, silent = true, priority = 50)
162+
public synchronized static Value textDeserialize(final Tool tool, final ExprOrOpArgNode[] args, final Context c,
163+
final TLCState s0, final TLCState s1, final int control, final CostModel cm) {
164+
165+
final String msgInvalidParam = "Deserialize error invalid parameters: ";
166+
167+
final RecordValue opts;
168+
169+
try {
170+
opts = (RecordValue) tool.eval(args[1], c, s0, s1, control, cm);
171+
} catch (Exception e){
172+
return new RecordValue(EXEC_NAMES, new Value[] { IntValue.ValOne, new StringValue(""), new StringValue(msgInvalidParam + e.toString()) }, false);
173+
}
174+
175+
final StringValue serializer = (StringValue) opts.apply(new StringValue("format"), EvalControl.Clear);
176+
if("TXT".equals(serializer.getVal().toString())) {
177+
178+
final StringValue filepath;
179+
final StringValue charset;
180+
181+
try {
182+
filepath = (StringValue) tool.eval(args[0], c, s0, s1, control, cm);
183+
charset = (StringValue) opts.apply(new StringValue("charset"), EvalControl.Clear);
184+
} catch(Exception e) {
185+
return new RecordValue(EXEC_NAMES, new Value[] { IntValue.ValOne, new StringValue(""), new StringValue(msgInvalidParam + e.toString()) }, false);
186+
}
187+
188+
try {
189+
final String result = Files.readString(
190+
Paths.get(filepath.getVal().toString()),
191+
Charset.forName(charset.getVal().toString()));
192+
193+
return new RecordValue(EXEC_NAMES, new Value[] { IntValue.ValZero, new StringValue(result), new StringValue("") }, false);
194+
195+
} catch(Exception e) {
196+
final StringValue errormsg = new StringValue("Deserialize error reading from the file: "+e.toString());
197+
return new RecordValue(EXEC_NAMES, new Value[] { IntValue.ValOne, new StringValue(""), errormsg }, false);
198+
}
199+
}
200+
201+
return null;
202+
}
203+
77204
static {
78205
// Eagerly lookup the environment, which is not going to change while the Java
79206
// process executes.

‎tests/IOUtilsTests.tla‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -138,4 +138,23 @@ ASSUME(LET ret == IOEnvExec([SOME_NESTED_VAR |-> "SOME_VAL", B |-> "23"],
138138
IN /\ PrintT(ret)
139139
/\ ret.exitValue = 0
140140
/\ ret.stderr = "")
141+
142+
---------------------------------------------------------------------------------------------------------------------------
143+
144+
ASSUME PrintT("IOUtilsTests!D")
145+
146+
ASSUME PrintT("IOUtilsTests!D!A")
147+
148+
file == "/tmp/txt-serialize-test.txt"
149+
payloadTXT == "Some text with \" escapes \" \\"
150+
151+
TXTSerializeResult == Serialize(payloadTXT, file, [format |-> "TXT", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "TRUNCATE_EXISTING">>])
152+
ASSUME(LET ret == TXTSerializeResult IN /\ ret.exitValue = 0
153+
/\ ret.stderr = "")
154+
155+
TXTDeserializeResult == Deserialize(file, [format |-> "TXT", charset |-> "UTF-8"])
156+
ASSUME(LET ret == TXTDeserializeResult IN /\ ret.exitValue = 0
157+
/\ ret.stdout = payloadTXT
158+
/\ ret.stderr = "")
159+
141160
=============================================================================

0 commit comments

Comments
 (0)