Skip to content

Commit 0074f87

Browse files
FedericoPonziFedericoPonzi
committed
Fix last quirks to make Slush formatted without changing the spec
1 parent 3bd7137 commit 0074f87

File tree

10 files changed

+77
-36
lines changed

10 files changed

+77
-36
lines changed

‎src/main/java/me/fponzi/tlaplusformatter/constructs/impl/AssumptionConstruct.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,14 +32,14 @@ public Doc buildDoc(TreeNode node, ConstructContext context, int indentSize) {
3232
var o = node.one();
3333
assert (o != null && o.length >= 2);
3434
var assume = context.buildChild(o[0]);
35-
var ret = assume.appendSpace(Doc.group(context.buildChild(o[1])).indent(o[0].getImage().length() + 1));
35+
var ret = assume.appendSpace(context.buildChild(o[1]).indent(o[0].getImage().length() + 1));
3636
if (o.length == 2) {
3737
return ret;
3838
}
3939
// More than one expression, need to handle line breaks
4040
// this is the case when ASSUME X == <expr>.
4141
ret = ret.appendSpace(context.buildChild(o[2])); // ==
42-
var content = Doc.group(context.buildChild(o[3])).indent(indentSize); // <expr>
42+
var content = context.buildChild(o[3]); // <expr>
4343
return ret.appendSpace(content);
4444
}
4545
}

‎src/main/java/me/fponzi/tlaplusformatter/constructs/impl/FcnApplConstruct.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ public Doc buildDoc(TreeNode node, ConstructContext context, int indentSize) {
5050

5151
return Doc.group(
5252
generalId.append(Doc.text("["))
53-
.appendLineOrEmpty(content.indent(indentSize))
53+
.appendLineOrEmpty(content).indent(indentSize)
5454
.appendLineOrEmpty(Doc.text("]"))
5555
);
5656
}

‎src/main/java/me/fponzi/tlaplusformatter/constructs/impl/OpApplicationConstruct.java‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,7 @@ public Doc buildDoc(TreeNode node, ConstructContext context, int indentSize) {
2727
//
2828
// z[0].format(f); // Head - GeneralId
2929
//z[1].format(f); // N_OpArgs
30-
return Doc
31-
.group(context.buildChild(z[0])
32-
.append(context.buildChild(z[1])));
30+
return context.buildChild(z[0])
31+
.append(context.buildChild(z[1]));
3332
}
3433
}

‎src/main/java/me/fponzi/tlaplusformatter/constructs/impl/OpArgsConstruct.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,13 +31,13 @@ public Doc buildDoc(TreeNode node, ConstructContext context, int indentSize) {
3131
if (z[i].getImage().equals(",") || z[i].getImage().equals(":")) {
3232
expr = expr.append(doc);
3333
} else {
34-
expr = expr.appendLineOrSpace(doc);
34+
expr = expr.appendSpace(doc);
3535
}
3636
}
3737
var lbracket = context.buildChild(z[0]); // (
3838
var rbracket = context.buildChild(z[z.length - 1]); // )
3939
return lbracket
40-
.append(Doc.group(expr).indent(indentSize))
41-
.appendLineOrEmpty(rbracket);
40+
.append(expr.indent(indentSize))
41+
.append(rbracket);
4242
}
4343
}

‎src/main/java/me/fponzi/tlaplusformatter/constructs/impl/SubsetOfConstruct.java‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -30,13 +30,13 @@ public Doc buildDoc(TreeNode node, ConstructContext context, int indentSize) {
3030
var z = node.zero();
3131
List<Doc> zDoc = Arrays.stream(z).map(context::buildChild).collect(Collectors.toList());
3232
return
33-
zDoc.get(0) // {
34-
.append(zDoc.get(1)) // x or a tuple like <<r,t>>
35-
.appendSpace(zDoc.get(2)) //\in
36-
.appendSpace(zDoc.get(3)) // S
37-
.append(zDoc.get(4)) // :
38-
.appendSpace(zDoc.get(5))
39-
.appendLineOrEmpty(zDoc.get(6))
40-
;
33+
Doc.group(
34+
zDoc.get(0) // {
35+
.append(zDoc.get(1)) // x or a tuple like <<r,t>>
36+
.appendSpace(zDoc.get(2)) //\in
37+
.appendSpace(zDoc.get(3)) // S
38+
.append(zDoc.get(4)) // :
39+
.appendSpace(zDoc.get(5).indent(indentSize)) // predicate
40+
.appendLineOrEmpty(zDoc.get(6)));
4141
}
4242
}

‎src/test/java/me/fponzi/tlaplusformatter/InputFolderTest.java‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,9 @@
11
package me.fponzi.tlaplusformatter;
22

3-
import org.junit.jupiter.api.Disabled;
43
import org.junit.jupiter.api.Test;
54

65
public class InputFolderTest extends LexiconTest {
76
@Test
8-
@Disabled
97
void testPlayground() {
108
testSpecFiles("Playground");
119
}
@@ -36,7 +34,6 @@ void testTowerOfHanoi() {
3634
}
3735

3836
@Test
39-
@Disabled
4037
// TODO: fix.
4138
void testSlush() {
4239
testSpecFiles("Slush");

‎src/test/java/me/fponzi/tlaplusformatter/LexiconTest.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ public void testSpecFiles(String name) {
2222
String inputSpec = Files.readString(Path.of(resource.toURI()));
2323
var f = new TLAPlusFormatter(input, new FormatConfig(80, 2));
2424
var actual = f.getOutput();
25-
System.out.println(f.getOutput());
25+
//System.out.println(f.getOutput());
2626
// commented until issues are fixed:
2727
compareOutputSpec(name, actual, f.root);
2828
} catch (Exception e) {
@@ -80,6 +80,7 @@ boolean compareAst(TreeNode root1, TreeNode root2) {
8080
if (root1.getKind() != root2.getKind()) {
8181
System.out.println("Node kinds do not match: " + root1.getKind() + " vs " + root2.getKind());
8282
System.out.println("Node image: " + root1.getImage() + " vs " + root2.getImage());
83+
System.out.println("Node Location" + root1.getLocation() + " vs " + root2.getLocation());
8384
}
8485
assertEquals(root1.getKind(), root2.getKind(), "Node kinds do not match");
8586
//assertEquals(root1.getImage(), root2.getImage());

‎src/test/resources/inputs/Playground.tla‎

Lines changed: 20 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,25 @@
11
---------------------- MODULE Playground ----------------------
2+
EXTENDS Naturals, FiniteSets, Sequences
23

3-
(* define statement *)
4-
Red == "Red"
4+
CONSTANTS Node,
5+
SlushLoopProcess,
6+
SlushQueryProcess,
7+
HostMapping,
8+
SlushIterationCount,
9+
SampleSetSize,
10+
PickFlipThreshold
511

6-
Red2 == "Red2"
12+
ASSUME /\ Cardinality(Node) = Cardinality(SlushLoopProcess)
13+
/\ Cardinality(Node) = Cardinality(SlushQueryProcess)
14+
/\ SlushIterationCount \in Nat
15+
/\ SampleSetSize \in Nat
16+
/\ PickFlipThreshold \in Nat
17+
18+
ASSUME HostMappingType == /\ Cardinality(Node) = Cardinality(HostMapping)
19+
/\ \A mapping \in HostMapping:
20+
/\ Cardinality(mapping) = 3
21+
/\ \E e \in mapping: e \in Node
22+
/\ \E e \in mapping: e \in SlushLoopProcess
23+
/\ \E e \in mapping: e \in SlushQueryProcess
724

825
==============================================================

‎src/test/resources/outputs/Playground.tla‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
---------------------- MODULE Playground ----------------------
2+
EXTENDS Naturals, FiniteSets, Sequences
3+
4+
CONSTANTS Node,
5+
SlushLoopProcess,
6+
SlushQueryProcess,
7+
HostMapping,
8+
SlushIterationCount,
9+
SampleSetSize,
10+
PickFlipThreshold
11+
12+
ASSUME /\ Cardinality(Node) = Cardinality(SlushLoopProcess)
13+
/\ Cardinality(Node) = Cardinality(SlushQueryProcess)
14+
/\ SlushIterationCount \in Nat
15+
/\ SampleSetSize \in Nat
16+
/\ PickFlipThreshold \in Nat
17+
18+
ASSUME HostMappingType == /\ Cardinality(Node) = Cardinality(HostMapping)
19+
/\ \A mapping \in HostMapping:
20+
/\ Cardinality(mapping) = 3
21+
/\ \E e \in mapping: e \in Node
22+
/\ \E e \in mapping: e \in SlushLoopProcess
23+
/\ \E e \in mapping: e \in SlushQueryProcess
24+
25+
==============================================================

‎src/test/resources/outputs/Slush.tla‎

Lines changed: 14 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -339,8 +339,8 @@ QuerySampleSet(self) ==
339339
LET otherNodes == Node \ { HostOf[self] }
340340
otherQueryProcesses ==
341341
{pid \in SlushQueryProcess: HostOf[pid] \in otherNodes}
342-
IN {pidSet \in
343-
SUBSET otherQueryProcesses: Cardinality(pidSet) = SampleSetSize
342+
IN {pidSet \in SUBSET otherQueryProcesses: Cardinality(pidSet) =
343+
SampleSetSize
344344
}:
345345
/\ sampleSet' = [sampleSet EXCEPT ![self] = possibleSampleSet]
346346
/\ message' =
@@ -361,17 +361,18 @@ TallyQueryReplies(self) ==
361361
/\ /\ \A pid \in sampleSet[self]:
362362
/\ \E msg \in PendingQueryReplyMessage(self): /\ msg.src = pid
363363
/\ LET redTally ==
364-
Cardinality({msg \in
365-
PendingQueryReplyMessage(self): /\ msg.src \in sampleSet[self]
366-
/\ msg.color = Red
367-
}
368-
)
364+
Cardinality({msg \in PendingQueryReplyMessage(self): /\ msg.src \in
365+
sampleSet[self]
366+
/\ msg.color = Red
367+
})
369368
IN LET blueTally ==
370-
Cardinality({msg \in
371-
PendingQueryReplyMessage(self): /\ msg.src \in sampleSet[self]
372-
/\ msg.color = Blue
373-
}
374-
)
369+
Cardinality({msg \in PendingQueryReplyMessage(self): /\ msg.src \in
370+
sampleSet[
371+
self
372+
]
373+
/\ msg.color =
374+
Blue
375+
})
375376
IN IF redTally >= PickFlipThreshold
376377
THEN /\ pick' = [pick EXCEPT ![HostOf[self]] = Red]
377378
ELSE /\ IF blueTally >= PickFlipThreshold
@@ -431,4 +432,5 @@ Spec == Init /\ [] [Next]_vars
431432
Termination == <> ( \A self \in ProcSet: pc[self] = "Done" )
432433

433434

435+
\* END TRANSLATION
434436
=============================================================================

0 commit comments

Comments
 (0)