Commit fc677465 authored by Benedikt Becker's avatar Benedikt Becker

Update bench/ce

parent 17bb76a2
......@@ -170,8 +170,8 @@ File record_one_field.mlw:
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 55:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
[previous iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "3" } }
Line 56:
x at L, [[@introduced], [@at:L], [@model_trace:x],
[@at:L:loc:location] =
......@@ -181,11 +181,12 @@ File record_one_field.mlw:
[@at:M:loc:location] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
[current iteration] x, [[@introduced], [@model_trace:x]] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
[current iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
bench/ce/record_one_field.mlw M test_loop'vc: Timeout or Unknown
Counter-example model:
......
......@@ -174,8 +174,8 @@ File record_one_field.mlw:
y, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "0" } }
Line 55:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
[previous iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "3" } }
Line 56:
x at L, [[@introduced], [@at:L], [@model_trace:x],
[@at:L:loc:location] =
......@@ -185,11 +185,12 @@ File record_one_field.mlw:
[@at:M:loc:location] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
[current iteration] x, [[@introduced], [@model_trace:x]] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
[current iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
bench/ce/record_one_field.mlw M test_loop'vc: Timeout or Unknown
Counter-example model:
......
......@@ -170,8 +170,8 @@ File record_one_field.mlw:
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 55:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
[previous iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "3" } }
Line 56:
x at L, [[@introduced], [@at:L], [@model_trace:x],
[@at:L:loc:location] =
......@@ -181,11 +181,12 @@ File record_one_field.mlw:
[@at:M:loc:location] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
[current iteration] x, [[@introduced], [@model_trace:x]] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
[current iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
bench/ce/record_one_field.mlw M test_loop'vc: Timeout or Unknown
Counter-example model:
......
......@@ -170,8 +170,8 @@ File record_one_field.mlw:
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 55:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "3" } }
[previous iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "3" } }
Line 56:
x at L, [[@introduced], [@at:L], [@model_trace:x],
[@at:L:loc:location] =
......@@ -181,11 +181,12 @@ File record_one_field.mlw:
[@at:M:loc:location] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
x, [[@introduced], [@model_trace:x]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
x, [[@introduced]] = {"proj_name" : "contents" , "type" : "Proj" ,
[current iteration] x, [[@introduced], [@model_trace:x]] =
{"proj_name" : "contents" , "type" : "Proj" ,
"value" : {"type" : "Integer" , "val" : "2" } }
Line 58:
[current iteration] x, [[@introduced]] = {"proj_name" : "contents" ,
"type" : "Proj" , "value" : {"type" : "Integer" , "val" : "2" } }
bench/ce/record_one_field.mlw M test_loop'vc: Timeout or Unknown
Counter-example model:
......
......@@ -174,8 +174,8 @@ File ref_ex.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 37:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 38:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -186,12 +186,13 @@ File ref_ex.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 40:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_ex.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -174,8 +174,8 @@ File ref_ex.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 37:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 38:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -186,12 +186,13 @@ File ref_ex.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 40:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_ex.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -174,8 +174,8 @@ File ref_ex.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 37:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 38:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -186,12 +186,13 @@ File ref_ex.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 40:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_ex.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -174,8 +174,8 @@ File ref_ex.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 37:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 38:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -186,12 +186,13 @@ File ref_ex.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 40:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_ex.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -193,8 +193,8 @@ File ref_mono.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 50:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 51:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -205,12 +205,13 @@ File ref_mono.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 53:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_mono.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -193,8 +193,8 @@ File ref_mono.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 50:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
Line 51:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -205,12 +205,13 @@ File ref_mono.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
Line 53:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
bench/ce/ref_mono.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -86,15 +86,15 @@ File ref_mono.mlw:
x23, [[@introduced], [@field:0:contents],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "-1" } }] } }
"value" : {"type" : "Integer" , "val" : "399" } }] } }
Line 38:
x23, [[@introduced], [@field:0:contents], [@model_trace:x23]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
"value" : {"type" : "Integer" , "val" : "401" } }] } }
old x23, [[@introduced], [@at:'Old], [@field:0:contents],
[@model_trace:x23], [@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "-1" } }] } }
"value" : {"type" : "Integer" , "val" : "399" } }] } }
old y, [[@introduced], [@at:'Old], [@field:0:contents], [@model_trace:y],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
......@@ -106,11 +106,11 @@ File ref_mono.mlw:
Line 41:
x23, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
"value" : {"type" : "Integer" , "val" : "400" } }] } }
Line 42:
x23, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
"value" : {"type" : "Integer" , "val" : "401" } }] } }
bench/ce/ref_mono.mlw M test_loop'vc: Timeout or Unknown
Counter-example model:
......@@ -193,8 +193,8 @@ File ref_mono.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "107" } }] } }
Line 50:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "54" } }] } }
Line 51:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -205,12 +205,13 @@ File ref_mono.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "107" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "53" } }] } }
Line 53:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "53" } }] } }
bench/ce/ref_mono.mlw M test_loop'vc: Timeout or Unknown
......
......@@ -86,15 +86,15 @@ File ref_mono.mlw:
x23, [[@introduced], [@field:0:contents],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "-1" } }] } }
"value" : {"type" : "Integer" , "val" : "399" } }] } }
Line 38:
x23, [[@introduced], [@field:0:contents], [@model_trace:x23]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
"value" : {"type" : "Integer" , "val" : "401" } }] } }
old x23, [[@introduced], [@at:'Old], [@field:0:contents],
[@model_trace:x23], [@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "-1" } }] } }
"value" : {"type" : "Integer" , "val" : "399" } }] } }
old y, [[@introduced], [@at:'Old], [@field:0:contents], [@model_trace:y],
[@at:'Old:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
......@@ -106,11 +106,11 @@ File ref_mono.mlw:
Line 41:
x23, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "0" } }] } }
"value" : {"type" : "Integer" , "val" : "400" } }] } }
Line 42:
x23, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "1" } }] } }
"value" : {"type" : "Integer" , "val" : "401" } }] } }
bench/ce/ref_mono.mlw M test_loop'vc: Timeout or Unknown
Counter-example model:
......@@ -193,8 +193,8 @@ File ref_mono.mlw:
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "107" } }] } }
Line 50:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[previous iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "54" } }] } }
Line 51:
x at L, [[@introduced], [@field:0:contents], [@at:L], [@model_trace:x],
......@@ -205,12 +205,13 @@ File ref_mono.mlw:
[@at:M:loc:location] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "107" } }] } }
x, [[@introduced], [@field:0:contents], [@model_trace:x]] =
[current iteration] x, [[@introduced], [@field:0:contents],
[@model_trace:x]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "53" } }] } }
Line 53:
x, [[@introduced], [@field:0:contents]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "contents" ,
[current iteration] x, [[@introduced], [@field:0:contents]] =
{"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
"value" : {"type" : "Integer" , "val" : "53" } }] } }
bench/ce/ref_mono.mlw M test_loop'vc: Timeout or Unknown
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment