302 lines
15 KiB
Promela
302 lines
15 KiB
Promela
@<EmacsMode "-*- preserves -*-">
|
|
@<Documentation [
|
|
"Individual test cases may be any of the following record types:"
|
|
<TestCaseTypes {
|
|
Test: {fields: [binary annotatedValue] expectations: #{1 2 3 4 5 6 7 8 9 11}}
|
|
NondeterministicTest: {fields: [binary annotatedValue] expectations: #{1 2 3 4 5 6 7 8 10 11}}
|
|
DecodeTest: {fields: [binary annotatedValue] expectations: #{1 2 3 4 5 6 7 8}}
|
|
ParseError: {fields: [text] expectations: #{12}}
|
|
ParseShort: {fields: [text] expectations: #{13}}
|
|
ParseEOF: {fields: [text] expectations: #{14}}
|
|
DecodeError: {fields: [bytes] expectations: #{15}}
|
|
DecodeShort: {fields: [bytes] expectations: #{16}}
|
|
DecodeEOF: {fields: [bytes] expectations: #{17}}
|
|
}>
|
|
"In each test, let value = strip(annotatedValue),",
|
|
" forward = value,",
|
|
" back = value,"
|
|
"except where test-case-specific values of `forward` and/or `back`",
|
|
"are provided by the executing harness, and check the following"
|
|
"numbered expectations according to the table above:"
|
|
<TestCaseExpectations {
|
|
1: "value = back"
|
|
2: "strip(decodeBinary(encodeBinary(value))) = back"
|
|
3: "strip(decodeBinary(encodeBinary(forward))) = back"
|
|
4: "strip(decodeBinary(binary)) = back"
|
|
5: "decodeBinary(binary) = annotatedValue"
|
|
6: "decodeBinary(encodeBinary(annotatedValue)) = annotatedValue"
|
|
7: "decodeText(encodeText(value)) = back"
|
|
8: "decodeText(encodeText(forward)) = back"
|
|
9: "encodeBinary(forward) = binary"
|
|
10: "canonicallyOrderedEncodedBinaryWithAnnotations(forward) = binary"
|
|
11: "encodeBinary(annotatedValue) = binary"
|
|
|
|
12: "decodeText(text) fails with a syntax error (NB. never with EOF)"
|
|
13: "decodeText(text) fails signalling premature EOF after partial parse (NB. never with a syntax error)"
|
|
14: "decodeText(text) fails signalling immediate EOF (NB. never with a syntax error)"
|
|
|
|
15: "decodeBinary(bytes) fails with a syntax error (NB. never with EOF)"
|
|
16: "decodeBinary(bytes) fails signalling premature EOF after partial parse (NB. never with a syntax error)"
|
|
17: "decodeBinary(bytes) fails signalling immediate EOF (NB. never with a syntax error)"
|
|
}>
|
|
"Implementations may vary in their treatment of the difference between expectations"
|
|
"13/14 and 16/17, depending on how they wish to treat end-of-stream conditions."
|
|
]>
|
|
<TestCases {
|
|
annotation1: <Test #x"BF 82A309 85A461626300" @"abc" 9>
|
|
annotation2: <Test #x"BF 8BA881A887BF81A883A47800 85A461626300 85A464656600" @"abc" @"def" [[] @"x" []]>
|
|
annotation3: <Test #x"BF 82A305 87BF82A30282A301 87BF82A30482A303" @@1 2 @@3 4 5>
|
|
annotation4: <NondeterministicTest #x"AA 88BF82A66183A6616B 88BF82A30183A66276 88BF82A66283A6626B 88BF82A30283A66276"
|
|
{@ak a: @av 1 @bk b: @bv 2}>
|
|
annotation5: <Test #x"BF8DA782A65288BF82A66683A6616683A66172" @ar <R @af f>>
|
|
annotation6: <Test #x"A788BF82A65283A6617288BF82A66683A66166" <@ar R @af f>>
|
|
annotation7:
|
|
;Stop reading symbols at @ -- this test has three separate annotations
|
|
<Test #x"BF81A882A66182A66282A663" @a@b@c[]>
|
|
bytes2: <Test #x"a568656c6c6f" #"hello">
|
|
bytes2a: <Test @"Internal whitespace is allowed, including commas!" #x"a5, 68, 65, 6c, 6c, 6f" #"hello">
|
|
bytes3: <Test #x"a5414243" #"ABC">
|
|
bytes4: <Test #x"a5414243" #x"414243">
|
|
bytes5: <Test #x"a5414a4e" #x" 41 4A 4e ">
|
|
bytes6: @"Bytes must be 2-digits entire" <ParseError "#x\"414 243\"">
|
|
bytes7: <Test #"\xa5corymb" #[Y29yeW1i]>
|
|
bytes8: <Test #"\xa5corymb" #[Y29 yeW 1i]>
|
|
bytes9: <Test #"\xa5Hi" #[SGk=]>
|
|
bytes10: <Test #"\xa5Hi" #[SGk]>
|
|
bytes11: <Test #"\xa5Hi" #[S G k]>
|
|
bytes12: @"Bytes syntax only supports \\x, not \\u" <ParseError "#\"\\u6c34\"">
|
|
bytes13: <Test #x"a5 61 62 63 6c 34 f0 5c 2f 22 08 0c 0a 0d 09 78 79 7a" #"abc\x6c\x34\xf0\\/\"\b\f\n\r\txyz">
|
|
|
|
dict0: <Test #x"aa" {}>
|
|
dict1: <NondeterministicTest #x"aa 83a46200 81a1 82a661 82a301 8aa882a30182a30282a303 82a563 99aa8ba666697273742d6e616d658ba4456c697a616265746800 96aa88a67375726e616d658ba4426c61636b77656c6c00" { a: 1 "b": #t [1 2 3]: #"c" { first-name: "Elizabeth" }: { surname: "Blackwell" } }>
|
|
dict2: @"Missing close brace" <ParseShort "{ a: b, c: d ">
|
|
dict2a: @"Missing close brace" <ParseShort "{">
|
|
dict3: @"Duplicate key" <ParseError "{ a: 1, a: 2 }">
|
|
dict4: @"Unexpected close brace" <ParseError "}">
|
|
dict5: @"Missing value" <DecodeError #x"aa 82a301 82a302 82a303">
|
|
double1: <Test #x"a23ff0000000000000" 1.0>
|
|
double2: <Test #x"a2fe3cb7b759bf0426" -1.202e300>
|
|
float1: <Test #x"a23f800000" 1.0f>
|
|
int-257: <Test #x"a3feff" -257>
|
|
int-256: <Test #x"a3ff00" -256>
|
|
int-255: <Test #x"a3ff01" -255>
|
|
int-254: <Test #x"a3ff02" -254>
|
|
int-129: <Test #x"a3ff7f" -129>
|
|
int-128: <Test #x"a380" -128>
|
|
int-127: <Test #x"a381" -127>
|
|
int-4: <Test #x"a3fc" -4>
|
|
int-3: <Test #x"a3fd" -3>
|
|
int-2: <Test #x"a3fe" -2>
|
|
int-1: <Test #x"a3ff" -1>
|
|
int0: <Test #x"a3" 0>
|
|
int1: <Test #x"a301" 1>
|
|
int12: <Test #x"a30c" 12>
|
|
int13: <Test #x"a30d" 13>
|
|
int127: <Test #x"a37f" 127>
|
|
int128: <Test #x"a30080" 128>
|
|
int255: <Test #x"a300ff" 255>
|
|
int256: <Test #x"a30100" 256>
|
|
int32767: <Test #x"a37fff" 32767>
|
|
int32768: <Test #x"a3008000" 32768>
|
|
int65535: <Test #x"a300ffff" 65535>
|
|
int65536: <Test #x"a3010000" 65536>
|
|
int131072: <Test #x"a3020000" 131072>
|
|
int2500000000: <Test #x"a3009502f900" 2500000000>
|
|
int87112285931760246646623899502532662132736: <Test #x"a3010000000000000000000000000000000000" 87112285931760246646623899502532662132736>
|
|
list0: <Test #x"a8" []>
|
|
list4: <Test #x"a882a30182a30282a30382a304" [1 2 3 4]>
|
|
list4a: <Test #x"a882a30182a30282a30382a304" [1, 2, 3, 4]>
|
|
list5: <Test #x"a882a3fe82a3ff81a382a301" [-2 -1 0 1]>
|
|
list6: <Test #x"a8 87a468656c6c6f00 86a67468657265 86a5776f726c64 81a8 81a9 81a1 81a0" ["hello" there #"world" [] #{} #t #f]>
|
|
list7: <Test #x"a8 84a6616263 84a62e2e2e 84a6646566" [abc ... def]>
|
|
list8: @"Missing close bracket" <ParseShort "[">
|
|
list9: @"Unexpected close bracket" <ParseError "]">
|
|
list10: @"Missing tag" <DecodeShort #x"a881">
|
|
noinput0: @"No input at all" <DecodeEOF #x"">
|
|
embed0: <Test #x"aba3" #!0>
|
|
embed1: <Test #x"ababa3" #!#!0>
|
|
embed2: <Test #x"a8 82aba3 88aba468656c6c6f00" [#!0 #!"hello"]>
|
|
record1: <Test #x"a7 88a663617074757265 8aa788a664697363617264" <capture <discard>>>
|
|
record2: <Test #x"a7 88a66f627365727665 a9a7 86a6737065616b 8aa788a664697363617264 95a7 88a663617074757265 8aa788a664697363617264" <observe <speak <discard>, <capture <discard>>>>>
|
|
record3: <Test #x"a7 9e a8 87a67469746c6564 87a6706572736f6e 82a302 86a67468696e67 82a301 82a365 8ba4426c61636b77656c6c00 91a7 85a664617465 83a3071d 82a302 82a303 84a4447200" <[titled person 2 thing 1] 101 "Blackwell" <date 1821 2 3> "Dr">>
|
|
record4: <Test #x"a788a664697363617264" <discard>>
|
|
record5: <Test #x"a782a30781a8" <7[]>>
|
|
record6: <Test #x"a788a66469736361726489a67375727072697365" <discard surprise>>
|
|
record7: <Test #x"a789a461537472696e670082a30382a304" <"aString" 3 4>>
|
|
record8: <Test #x"a78aa788a66469736361726482a30382a304" <<discard> 3 4>>
|
|
record9: @"Missing record label" <ParseError "<>">
|
|
record10: @"Missing close-angle-bracket" <ParseShort "<">
|
|
record11: @"Unexpected close-angle-bracket" <ParseError ">">
|
|
set0: <Test #x"a9" #{}>
|
|
set1: <NondeterministicTest #x"a982a30182a30282a303" #{1 2 3}>
|
|
set2: @"Missing close brace" <ParseShort "#{ 1 2 3 ">
|
|
set2a: @"Missing close brace" <ParseShort "#{">
|
|
set3: @"Duplicate value" <ParseError "#{a a}">
|
|
string0: <Test #x"a400" "">
|
|
string3: <Test #x"a468656c6c6f00" "hello">
|
|
string4: <Test #x"a4616263e6b0b4e6b0b45c2f22080c0a0d0978797a00" "abc\u6c34\u6C34\\/\"\b\f\n\r\txyz">
|
|
string5: <Test #x"a4f09d849e00" "\uD834\uDD1E">
|
|
symbol0: <Test #x"a6" ||>
|
|
symbol2: <Test #x"a668656c6c6f" hello>
|
|
tag1: @"Invalid tag" <DecodeError #x"10">
|
|
tag2: @"Invalid tag" <DecodeError #x"61a30110">
|
|
whitespace0: @"Leading spaces have to eventually yield something" <ParseShort " ">
|
|
whitespace1: @"No input at all" <ParseEOF "">
|
|
value1: <Test #"\xA5corymb" #=#"\xA5corymb">
|
|
value2: <Test #"\xA1" #=#"\xA1">
|
|
value3: <Test #"\xA1" #=#[oQ]>
|
|
value4: <Test #"\xA1" #=#[oQ==]>
|
|
value5: <Test #"\xA1" #= #[oQ==]>
|
|
value6: <Test #x"A882A30182A30282A303" #=#x"A882A30182A30282A303">
|
|
|
|
longlist14: <Test #x"a881a081a081a081a081a081a081a081a081a081a081a081a081a081a0"
|
|
[#f #f #f #f #f
|
|
#f #f #f #f #f
|
|
#f #f #f #f]>
|
|
longlist15: <Test #x"a881a081a081a081a081a081a081a081a081a081a081a081a081a081a081a0"
|
|
[#f #f #f #f #f
|
|
#f #f #f #f #f
|
|
#f #f #f #f #f]>
|
|
longlist100:
|
|
<Test #x"a8
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0"
|
|
[#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f]>
|
|
longlist200:
|
|
<Test #x"a8
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0
|
|
81a081a081a081a081a081a081a081a081a081a0"
|
|
[#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f
|
|
#f #f #f #f #f #f #f #f #f #f]>
|
|
|
|
rfc8259-example1: <NondeterministicTest
|
|
#x"AA
|
|
87 A4 496D61676500
|
|
01B7 AA
|
|
8A A4 416E696D6174656400 86 A6 66616C7365
|
|
88 A4 48656967687400 83 A3 0258
|
|
85 A4 49447300 91 A8
|
|
82 A3 74
|
|
83 A3 03AF
|
|
83 A3 00EA
|
|
84 A3 009789
|
|
8B A4 5468756D626E61696C00 C7 AA
|
|
88 A4 48656967687400 82 A3 7D
|
|
85 A4 55726C00 A8 A4 687474703A2F2F7777772E6578616D706C652E636F6D2F696D6167652F34383139383939343300
|
|
87 A4 576964746800 82 A3 64
|
|
87 A4 5469746C6500 96 A4 566965772066726F6D203135746820466C6F6F7200
|
|
87 A4 576964746800 83 A3 0320"
|
|
{
|
|
"Image": {
|
|
"Width": 800,
|
|
"Height": 600,
|
|
"Title": "View from 15th Floor",
|
|
"Thumbnail": {
|
|
"Url": "http://www.example.com/image/481989943",
|
|
"Height": 125,
|
|
"Width": 100
|
|
},
|
|
"Animated" : false,
|
|
"IDs": [116, 943, 234, 38793]
|
|
}
|
|
}>
|
|
|
|
rfc8259-example2: <NondeterministicTest
|
|
#x"a8
|
|
018c aa
|
|
89 a4 4164647265737300 82 a4 00
|
|
86 a4 4369747900 8f a4 53414e204652414e434953434f00
|
|
89 a4 436f756e74727900 84 a4 555300
|
|
8a a4 4c6174697475646500 89 a2 4042e226809d4952
|
|
8b a4 4c6f6e67697475646500 89 a2 c05e99566cf41f21
|
|
87 a4 537461746500 84 a4 434100
|
|
85 a4 5a697000 87 a4 393431303700
|
|
8b a4 707265636973696f6e00 85 a4 7a697000
|
|
0188 aa
|
|
89 a4 4164647265737300 82 a4 00
|
|
86 a4 4369747900 8b a4 53554e4e5956414c4500
|
|
89 a4 436f756e74727900 84 a4 555300
|
|
8a a4 4c6174697475646500 89 a2 4042af9d66adb403
|
|
8b a4 4c6f6e67697475646500 89 a2 c05e81aa4fca42af
|
|
87 a4 537461746500 84 a4 434100
|
|
85 a4 5a697000 87 a4 393430383500
|
|
8b a4 707265636973696f6e00 85 a4 7a697000"
|
|
[
|
|
{
|
|
"precision": "zip",
|
|
"Latitude": 37.7668,
|
|
"Longitude": -122.3959,
|
|
"Address": "",
|
|
"City": "SAN FRANCISCO",
|
|
"State": "CA",
|
|
"Zip": "94107",
|
|
"Country": "US"
|
|
},
|
|
{
|
|
"precision": "zip",
|
|
"Latitude": 37.371991,
|
|
"Longitude": -122.026020,
|
|
"Address": "",
|
|
"City": "SUNNYVALE",
|
|
"State": "CA",
|
|
"Zip": "94085",
|
|
"Country": "US"
|
|
}
|
|
]>
|
|
|
|
}
|
|
>
|