Add a CBOR module that reads and writes TLA+ values

README.md

@@ -13,6 +13,7 @@ The Modules
 | ---: | ---- | :--: | ---- |
 | [`BagsExt.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/BagsExt.tla) | Additional operators on bags (e.g. `BagAdd`, `BagRemove`, `FoldBag`, etc.) | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/BagsExt.java) | [@muenchnerkindl](https://github.com/muenchnerkindl), [@lemmy](https://github.com/lemmy) |
 | [`Bitwise.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Bitwise.tla) | Bitwise And and shift-right. | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Bitwise.java) | [@lemmy](https://github.com/lemmy), [@pfeodrippe](https://github.com/pfeodrippe) |
+| [`CBOR.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/CBOR.tla) | CBOR (RFC 8949) encoding and decoding of TLA+ values, in memory or in files, including sets, model values, and functions. | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/CBOR.java) | [@younes-io](https://github.com/younes-io) |
 | [`Combinatorics.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Combinatorics.tla) | Binomial coefficient (N choose K) and factorial operator | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Combinatorics.java) | [@lemmy](https://github.com/lemmy) |
 | [`CSV.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/CSV.tla) | Operations on CSV files  | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/CSV.java) | [@lemmy](https://github.com/lemmy) |
 | [`DifferentialEquations.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/DifferentialEquations.tla) | see page 178 of [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf) | | Leslie Lamport |
@@ -41,7 +42,7 @@ appear in module `MTheorems.tla`, and proofs of these theorems can be found in `
 How to use it
 -------------
 
-You must be running [Java 9 or higher](https://github.com/tlaplus/CommunityModules/issues/34#issuecomment-756571840).
+You must be running Java 11 or higher.
 
 Just copy & paste the snippet, the operators, or the set of modules you are interested in.
 

build.xml

@@ -29,9 +29,11 @@
 
 	<target name="compile" depends="download" description="compile the java module overwrites">
 		<javac srcdir="${src}" destdir="${build}/modules" classpath="${tlc}/tla2tools.jar:${lib}/gson-2.8.6.jar:${lib}/jgrapht-core-1.5.1.jar:${lib}/jungrapht-layout-1.4-SNAPSHOT.jar:${lib}/slf4j-api-1.7.30.jar:${lib}/slf4j-nop-1.7.30.jar:${lib}/commons-lang3-3.12.0.jar:${lib}/commons-math3-3.6.1.jar"
-           source="1.8"
-           target="1.8"
+           release="11"
            deprecation="true"
+           includeantruntime="false"/>
+		<javac srcdir="${src-test}" destdir="${build}/tests" classpath="${lib}/junit-4.13.jar"
+           release="11"
            includeantruntime="false"/>
 	</target>
 
@@ -103,6 +105,17 @@
 	</target>
 
 	<target name="test" depends="dist" description="Run the modules in tests/ on the TLA+ modules in dist/">
+		<!-- Check the golden bytes in tests/CBORTests.tla against a second CBOR encoder. -->
+		<java classname="org.junit.runner.JUnitCore" fork="true" failonerror="true">
+			<sysproperty key="basepath" value="${basedir}/tests"/>
+			<arg value="tlc2.overrides.CBORGoldenTest"/>
+			<classpath>
+				<pathelement location="${build}/tests" />
+				<pathelement location="${lib}/junit-4.13.jar" />
+				<pathelement location="${lib}/hamcrest-core-1.3.jar" />
+			</classpath>
+		</java>
+
 		<!-- On Unix, run AllTestsUnix which includes IOExec/shell tests; on Windows, run AllTests only. -->
 		<condition property="allTests" value="${basedir}/tests/AllTestsUnix">
 			<not><os family="windows"/></not>

modules/CBOR.tla

@@ -0,0 +1,64 @@
+-------------------------------- MODULE CBOR --------------------------------
+(***************************************************************************)
+(* Encodes TLA+ values as CBOR (RFC 8949) and decodes them back.             *)
+(* CBORSerialize and CBORDeserialize exchange values through files.         *)
+(* Public ToCBOR and FromCBOR work in memory, without file I/O.             *)
+(* ToCBOR returns a sequence of integers in 0..255, one per encoded byte.   *)
+(* Use its length to check message sizes, or FromCBOR to interpret bytes.  *)
+(*                                                                         *)
+(* In a module that uses CBOR:                                              *)
+(*   EXTENDS Naturals, Sequences, CBOR                                     *)
+(*   Message == [id |-> 1, payload |-> <<TRUE, FALSE>>]                    *)
+(*   Fits == Len(ToCBOR(Message)) <= 1024                                  *)
+(*   Decoded == FromCBOR(<<130, 1, 245>>)   \* equals <<1, TRUE>>         *)
+(*                                                                         *)
+(* For files, using the same imports and Message definition:               *)
+(*   WriteMessage == CBORSerialize("/tmp/message.cbor", Message)           *)
+(*   ReadMessage == CBORDeserialize("/tmp/message.cbor")                   *)
+(*                                                                         *)
+(* Requires CommunityModules.jar or CommunityModules-deps.jar on TLC's    *)
+(* classpath. See README.md for setup.                                     *)
+(* Values must be finite and encodable: integers within TLC's range and    *)
+(* strings of valid Unicode.  Set elements and function arguments must be  *)
+(* comparable by TLC for FromCBOR(ToCBOR(v)) = v to hold.  Deep nesting    *)
+(* can exhaust the JVM stack, which a larger -Xss setting can relieve.     *)
+(***************************************************************************)
+
+LOCAL INSTANCE TLC
+
+(***************************************************************************)
+(* The CBOR encoding of value as a sequence of integers in 0..255, one     *)
+(* per byte.  Sets use tag 258, model values tag 39, and functions that    *)
+(* are neither sequences nor records tag 33000 (registered with IANA).     *)
+(* Equal values give identical bytes.  TLC reports an error if value       *)
+(* cannot be encoded.                                                      *)
+(***************************************************************************)
+ToCBOR(value) ==
+  Assert(FALSE, "ToCBOR needs CommunityModules.jar on TLC's classpath.")
+
+(***************************************************************************)
+(* The TLA+ value of the CBOR data item in bytes, a sequence of integers   *)
+(* in 0..255.  TLC reports an error for malformed input and for anything   *)
+(* it cannot represent, such as floats or a model value it does not know.  *)
+(***************************************************************************)
+FromCBOR(bytes) ==
+  Assert(FALSE, "FromCBOR needs CommunityModules.jar on TLC's classpath.")
+
+(***************************************************************************)
+(* Writes the bytes of ToCBOR(value) to the file absoluteFilename and      *)
+(* equals TRUE.  Creates missing parent directories and replaces an        *)
+(* existing file.  If value cannot be encoded, TLC reports an error and    *)
+(* leaves the file untouched.                                              *)
+(***************************************************************************)
+CBORSerialize(absoluteFilename, value) ==
+  Assert(FALSE, "CBORSerialize needs CommunityModules.jar on TLC's classpath.")
+
+(***************************************************************************)
+(* FromCBOR applied to the bytes of the file absoluteFilename.  A          *)
+(* definition without parameters is constant-level, so TLC reuses its      *)
+(* value instead of reading the file again in each state.                  *)
+(***************************************************************************)
+CBORDeserialize(absoluteFilename) ==
+  Assert(FALSE, "CBORDeserialize needs CommunityModules.jar on TLC's classpath.")
+
+=============================================================================