Converted cav benchmarks with termination property for lola and sara

0e10c59e · Philipp Meyer · c51c68df · 0e10c59e · 0e10c59e · 0e10c59e
Commit 0e10c59e authored Jul 25, 2014 by Philipp Meyer
165 changed files
--- a/benchmarks/cav-benchmarks/mist/PN/MultiME.spec.terminating
+++ b/benchmarks/cav-benchmarks/mist/PN/MultiME.spec.terminating
+PLACE 'sigma,'m1,'m2,x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,'x0,'x1,'x2,'x3,'x4,'x5,'x6,'x7,'x8,'x9,'x10,'x11;
+
+MARKING 'm1:1,'x1:1,'x2:1,'x5:1,'x6:1,'x9:1,x1:1,x2:1,x5:1,x6:1,x9:1;
+
+TRANSITION 'switch
+CONSUME 'm1:1;
+PRODUCE 'm2:1;
+
+TRANSITION 't1
+CONSUME 'x0:1,'x1:1,'x2:1,x0:1,x1:1,x2:1,'m1:1;
+PRODUCE 'x1:1,'x3:1,x1:1,x3:1,'m1:1;
+
+TRANSITION ''t1
+CONSUME 'x0:1,'x1:1,'x2:1,'m2:1;
+PRODUCE 'x1:1,'x3:1,'sigma:1,'m2:1;
+
+TRANSITION 't2
+CONSUME 'x0:1,'x1:1,'x2:1,x0:1,x1:1,x2:1,'m1:1;
+PRODUCE 'x2:1,'x4:1,x2:1,x4:1,'m1:1;
+
+TRANSITION ''t2
+CONSUME 'x0:1,'x1:1,'x2:1,'m2:1;
+PRODUCE 'x2:1,'x4:1,'sigma:1,'m2:1;
+
+TRANSITION 't3
+CONSUME 'x3:1,x3:1,'m1:1;
+PRODUCE 'x0:1,'x2:1,x0:1,x2:1,'m1:1;
+
+TRANSITION ''t3
+CONSUME 'x3:1,'m2:1;
+PRODUCE 'x0:1,'x2:1,'sigma:1,'m2:1;
+
+TRANSITION 't4
+CONSUME 'x4:1,x4:1,'m1:1;
+PRODUCE 'x0:1,'x1:1,x0:1,x1:1,'m1:1;
+
+TRANSITION ''t4
+CONSUME 'x4:1,'m2:1;
+PRODUCE 'x0:1,'x1:1,'sigma:1,'m2:1;
+
+TRANSITION 't5
+CONSUME 'x0:1,'x5:1,'x6:1,x0:1,x5:1,x6:1,'m1:1;
+PRODUCE 'x5:1,'x7:1,x5:1,x7:1,'m1:1;
+
+TRANSITION ''t5
+CONSUME 'x0:1,'x5:1,'x6:1,'m2:1;
+PRODUCE 'x5:1,'x7:1,'sigma:1,'m2:1;
+
+TRANSITION 't6
+CONSUME 'x0:1,'x5:1,'x6:1,x0:1,x5:1,x6:1,'m1:1;
+PRODUCE 'x6:1,'x8:1,x6:1,x8:1,'m1:1;
+
+TRANSITION ''t6
+CONSUME 'x0:1,'x5:1,'x6:1,'m2:1;
+PRODUCE 'x6:1,'x8:1,'sigma:1,'m2:1;
+
+TRANSITION 't7
+CONSUME 'x7:1,x7:1,'m1:1;
+PRODUCE 'x0:1,'x6:1,x0:1,x6:1,'m1:1;
+
+TRANSITION ''t7
+CONSUME 'x7:1,'m2:1;
+PRODUCE 'x0:1,'x6:1,'sigma:1,'m2:1;
+
+TRANSITION 't8
+CONSUME 'x8:1,x8:1,'m1:1;
+PRODUCE 'x0:1,'x5:1,x0:1,x5:1,'m1:1;
+
+TRANSITION ''t8
+CONSUME 'x8:1,'m2:1;
+PRODUCE 'x0:1,'x5:1,'sigma:1,'m2:1;
+
+TRANSITION 't9
+CONSUME 'x9:1,x9:1,'m1:1;
+PRODUCE 'x10:1,x10:1,'m1:1;
+
+TRANSITION ''t9
+CONSUME 'x9:1,'m2:1;
+PRODUCE 'x10:1,'sigma:1,'m2:1;
+
+TRANSITION 't10
+CONSUME 'x10:1,x10:1,'m1:1;
+PRODUCE 'x11:1,x11:1,'m1:1;
+
+TRANSITION ''t10
+CONSUME 'x10:1,'m2:1;
+PRODUCE 'x11:1,'sigma:1,'m2:1;
+
+TRANSITION 't11
+CONSUME 'x11:1,x11:1,'m1:1;
+PRODUCE 'x0:1,'x10:1,x0:1,x10:1,'m1:1;
+
+TRANSITION ''t11
+CONSUME 'x11:1,'m2:1;
+PRODUCE 'x0:1,'x10:1,'sigma:1,'m2:1;
+
--- a/benchmarks/cav-benchmarks/mist/PN/MultiME.spec.terminating.sara
+++ b/benchmarks/cav-benchmarks/mist/PN/MultiME.spec.terminating.sara
+PROBLEM termination_by_reachability:
+GOAL REACHABILITY;
+FILE MultiME.spec.terminating TYPE LOLA;
+INITIAL 'm1:1,'x1:1,'x2:1,'x5:1,'x6:1,'x9:1,x1:1,x2:1,x5:1,x6:1,x9:1;
+FINAL COVER;
+CONSTRAINTS 'sigma>1,'x0+-1x0>0,'x1+-1x1>0,'x2+-1x2>0,'x3+-1x3>0,'x4+-1x4>0,'x5+-1x5>0,'x6+-1x6>0,'x7+-1x7>0,'x8+-1x8>0,'x9+-1x9>0,'x10+-1x10>0,'x11+-1x11>0;
--- a/benchmarks/cav-benchmarks/mist/PN/MultiME.spec.terminating.task1
+++ b/benchmarks/cav-benchmarks/mist/PN/MultiME.spec.terminating.task1
+EF ('sigma >= 1 AND ('x0 - x0) >= 0 AND ('x1 - x1) >= 0 AND ('x2 - x2) >= 0 AND ('x3 - x3) >= 0 AND ('x4 - x4) >= 0 AND ('x5 - x5) >= 0 AND ('x6 - x6) >= 0 AND ('x7 - x7) >= 0 AND ('x8 - x8) >= 0 AND ('x9 - x9) >= 0 AND ('x10 - x10) >= 0 AND ('x11 - x11) >= 0)
--- a/benchmarks/cav-benchmarks/mist/PN/basicME.spec.terminating
+++ b/benchmarks/cav-benchmarks/mist/PN/basicME.spec.terminating
+PLACE 'sigma,'m1,'m2,x0,x1,x2,x3,x4,'x0,'x1,'x2,'x3,'x4;
+
+MARKING 'm1:1,'x0:1,'x1:1,'x2:1,x0:1,x1:1,x2:1;
+
+TRANSITION 'switch
+CONSUME 'm1:1;
+PRODUCE 'm2:1;
+
+TRANSITION 'init1
+CONSUME 'm1:1;
+PRODUCE 'x0:1,x0:1,'m1:1;
+
+TRANSITION 't1
+CONSUME 'x0:1,'x1:1,'x2:1,x0:1,x1:1,x2:1,'m1:1;
+PRODUCE 'x1:1,'x3:1,x1:1,x3:1,'m1:1;
+
+TRANSITION ''t1
+CONSUME 'x0:1,'x1:1,'x2:1,'m2:1;
+PRODUCE 'x1:1,'x3:1,'sigma:1,'m2:1;
+
+TRANSITION 't2
+CONSUME 'x0:1,'x1:1,'x2:1,x0:1,x1:1,x2:1,'m1:1;
+PRODUCE 'x2:1,'x4:1,x2:1,x4:1,'m1:1;
+
+TRANSITION ''t2
+CONSUME 'x0:1,'x1:1,'x2:1,'m2:1;
+PRODUCE 'x2:1,'x4:1,'sigma:1,'m2:1;
+
+TRANSITION 't3
+CONSUME 'x3:1,x3:1,'m1:1;
+PRODUCE 'x0:1,'x2:1,x0:1,x2:1,'m1:1;
+
+TRANSITION ''t3
+CONSUME 'x3:1,'m2:1;
+PRODUCE 'x0:1,'x2:1,'sigma:1,'m2:1;
+
+TRANSITION 't4
+CONSUME 'x4:1,x4:1,'m1:1;
+PRODUCE 'x0:1,'x1:1,x0:1,x1:1,'m1:1;
+
+TRANSITION ''t4
+CONSUME 'x4:1,'m2:1;
+PRODUCE 'x0:1,'x1:1,'sigma:1,'m2:1;
+
--- a/benchmarks/cav-benchmarks/mist/PN/basicME.spec.terminating.sara
+++ b/benchmarks/cav-benchmarks/mist/PN/basicME.spec.terminating.sara
+PROBLEM termination_by_reachability:
+GOAL REACHABILITY;
+FILE basicME.spec.terminating TYPE LOLA;
+INITIAL 'm1:1,'x0:1,'x1:1,'x2:1,x0:1,x1:1,x2:1;
+FINAL COVER;
+CONSTRAINTS 'sigma>1,'x0+-1x0>0,'x1+-1x1>0,'x2+-1x2>0,'x3+-1x3>0,'x4+-1x4>0;
--- a/benchmarks/cav-benchmarks/mist/PN/basicME.spec.terminating.task1
+++ b/benchmarks/cav-benchmarks/mist/PN/basicME.spec.terminating.task1
+EF ('sigma >= 1 AND ('x0 - x0) >= 0 AND ('x1 - x1) >= 0 AND ('x2 - x2) >= 0 AND ('x3 - x3) >= 0 AND ('x4 - x4) >= 0)
--- a/benchmarks/cav-benchmarks/mist/PN/bingham_h150.spec.terminating
+++ b/benchmarks/cav-benchmarks/mist/PN/bingham_h150.spec.terminating
+PLACE 'sigma,'m1,'m2,x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48,x49,x50,x51,x52,x53,x54,x55,x56,x57,x58,x59,x60,x61,x62,x63,x64,x65,x66,x67,x68,x69,x70,x71,x72,x73,x74,x75,x76,x77,x78,x79,x80,x81,x82,x83,x84,x85,x86,x87,x88,x89,x90,x91,x92,x93,x94,x95,x96,x97,x98,x99,x100,x101,x102,x103,x104,x105,x106,x107,x108,x109,x110,x111,x112,x113,x114,x115,x116,x117,x118,x119,x120,x121,x122,x123,x124,x125,x126,x127,x128,x129,x130,x131,x132,x133,x134,x135,x136,x137,x138,x139,x140,x141,x142,x143,x144,x145,x146,x147,x148,x149,x150,x151,x152,'x0,'x1,'x2,'x3,'x4,'x5,'x6,'x7,'x8,'x9,'x10,'x11,'x12,'x13,'x14,'x15,'x16,'x17,'x18,'x19,'x20,'x21,'x22,'x23,'x24,'x25,'x26,'x27,'x28,'x29,'x30,'x31,'x32,'x33,'x34,'x35,'x36,'x37,'x38,'x39,'x40,'x41,'x42,'x43,'x44,'x45,'x46,'x47,'x48,'x49,'x50,'x51,'x52,'x53,'x54,'x55,'x56,'x57,'x58,'x59,'x60,'x61,'x62,'x63,'x64,'x65,'x66,'x67,'x68,'x69,'x70,'x71,'x72,'x73,'x74,'x75,'x76,'x77,'x78,'x79,'x80,'x81,'x82,'x83,'x84,'x85,'x86,'x87,'x88,'x89,'x90,'x91,'x92,'x93,'x94,'x95,'x96,'x97,'x98,'x99,'x100,'x101,'x102,'x103,'x104,'x105,'x106,'x107,'x108,'x109,'x110,'x111,'x112,'x113,'x114,'x115,'x116,'x117,'x118,'x119,'x120,'x121,'x122,'x123,'x124,'x125,'x126,'x127,'x128,'x129,'x130,'x131,'x132,'x133,'x134,'x135,'x136,'x137,'x138,'x139,'x140,'x141,'x142,'x143,'x144,'x145,'x146,'x147,'x148,'x149,'x150,'x151,'x152;
+
+MARKING 'm1:1,'x0:1,'x152:1,x0:1,x152:1;
+
+TRANSITION 'switch
+CONSUME 'm1:1;
+PRODUCE 'm2:1;
+
+TRANSITION 'init1
+CONSUME 'm1:1;
+PRODUCE 'x0:1,x0:1,'m1:1;
+
+TRANSITION 't1
+CONSUME 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+PRODUCE 'x1:1,'x151:1,x1:1,x151:1,'m1:1;
+
+TRANSITION ''t1
+CONSUME 'x0:1,'x152:1,'m2:1;
+PRODUCE 'x1:1,'x151:1,'sigma:1,'m2:1;
+
+TRANSITION 't2
+CONSUME 'x1:1,'x152:1,x1:1,x152:1,'m1:1;
+PRODUCE 'x0:1,'x151:1,x0:1,x151:1,'m1:1;
+
+TRANSITION ''t2
+CONSUME 'x1:1,'x152:1,'m2:1;
+PRODUCE 'x0:1,'x151:1,'sigma:1,'m2:1;
+
+TRANSITION 't3
+CONSUME 'x1:1,'x151:1,x1:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t3
+CONSUME 'x1:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't4
+CONSUME 'x1:1,x1:1,'m1:1;
+PRODUCE 'x2:1,x2:1,'m1:1;
+
+TRANSITION ''t4
+CONSUME 'x1:1,'m2:1;
+PRODUCE 'x2:1,'sigma:1,'m2:1;
+
+TRANSITION 't5
+CONSUME 'x2:1,'x151:1,x2:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t5
+CONSUME 'x2:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't6
+CONSUME 'x2:1,x2:1,'m1:1;
+PRODUCE 'x3:1,x3:1,'m1:1;
+
+TRANSITION ''t6
+CONSUME 'x2:1,'m2:1;
+PRODUCE 'x3:1,'sigma:1,'m2:1;
+
+TRANSITION 't7
+CONSUME 'x3:1,'x151:1,x3:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t7
+CONSUME 'x3:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't8
+CONSUME 'x3:1,x3:1,'m1:1;
+PRODUCE 'x4:1,x4:1,'m1:1;
+
+TRANSITION ''t8
+CONSUME 'x3:1,'m2:1;
+PRODUCE 'x4:1,'sigma:1,'m2:1;
+
+TRANSITION 't9
+CONSUME 'x4:1,'x151:1,x4:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t9
+CONSUME 'x4:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't10
+CONSUME 'x4:1,x4:1,'m1:1;
+PRODUCE 'x5:1,x5:1,'m1:1;
+
+TRANSITION ''t10
+CONSUME 'x4:1,'m2:1;
+PRODUCE 'x5:1,'sigma:1,'m2:1;
+
+TRANSITION 't11
+CONSUME 'x5:1,'x151:1,x5:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t11
+CONSUME 'x5:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't12
+CONSUME 'x5:1,x5:1,'m1:1;
+PRODUCE 'x6:1,x6:1,'m1:1;
+
+TRANSITION ''t12
+CONSUME 'x5:1,'m2:1;
+PRODUCE 'x6:1,'sigma:1,'m2:1;
+
+TRANSITION 't13
+CONSUME 'x6:1,'x151:1,x6:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t13
+CONSUME 'x6:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't14
+CONSUME 'x6:1,x6:1,'m1:1;
+PRODUCE 'x7:1,x7:1,'m1:1;
+
+TRANSITION ''t14
+CONSUME 'x6:1,'m2:1;
+PRODUCE 'x7:1,'sigma:1,'m2:1;
+
+TRANSITION 't15
+CONSUME 'x7:1,'x151:1,x7:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t15
+CONSUME 'x7:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't16
+CONSUME 'x7:1,x7:1,'m1:1;
+PRODUCE 'x8:1,x8:1,'m1:1;
+
+TRANSITION ''t16
+CONSUME 'x7:1,'m2:1;
+PRODUCE 'x8:1,'sigma:1,'m2:1;
+
+TRANSITION 't17
+CONSUME 'x8:1,'x151:1,x8:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t17
+CONSUME 'x8:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't18
+CONSUME 'x8:1,x8:1,'m1:1;
+PRODUCE 'x9:1,x9:1,'m1:1;
+
+TRANSITION ''t18
+CONSUME 'x8:1,'m2:1;
+PRODUCE 'x9:1,'sigma:1,'m2:1;
+
+TRANSITION 't19
+CONSUME 'x9:1,'x151:1,x9:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t19
+CONSUME 'x9:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't20
+CONSUME 'x9:1,x9:1,'m1:1;
+PRODUCE 'x10:1,x10:1,'m1:1;
+
+TRANSITION ''t20
+CONSUME 'x9:1,'m2:1;
+PRODUCE 'x10:1,'sigma:1,'m2:1;
+
+TRANSITION 't21
+CONSUME 'x10:1,'x151:1,x10:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t21
+CONSUME 'x10:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't22
+CONSUME 'x10:1,x10:1,'m1:1;
+PRODUCE 'x11:1,x11:1,'m1:1;
+
+TRANSITION ''t22
+CONSUME 'x10:1,'m2:1;
+PRODUCE 'x11:1,'sigma:1,'m2:1;
+
+TRANSITION 't23
+CONSUME 'x11:1,'x151:1,x11:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t23
+CONSUME 'x11:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't24
+CONSUME 'x11:1,x11:1,'m1:1;
+PRODUCE 'x12:1,x12:1,'m1:1;
+
+TRANSITION ''t24
+CONSUME 'x11:1,'m2:1;
+PRODUCE 'x12:1,'sigma:1,'m2:1;
+
+TRANSITION 't25
+CONSUME 'x12:1,'x151:1,x12:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t25
+CONSUME 'x12:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't26
+CONSUME 'x12:1,x12:1,'m1:1;
+PRODUCE 'x13:1,x13:1,'m1:1;
+
+TRANSITION ''t26
+CONSUME 'x12:1,'m2:1;
+PRODUCE 'x13:1,'sigma:1,'m2:1;
+
+TRANSITION 't27
+CONSUME 'x13:1,'x151:1,x13:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t27
+CONSUME 'x13:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't28
+CONSUME 'x13:1,x13:1,'m1:1;
+PRODUCE 'x14:1,x14:1,'m1:1;
+
+TRANSITION ''t28
+CONSUME 'x13:1,'m2:1;
+PRODUCE 'x14:1,'sigma:1,'m2:1;
+
+TRANSITION 't29
+CONSUME 'x14:1,'x151:1,x14:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t29
+CONSUME 'x14:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't30
+CONSUME 'x14:1,x14:1,'m1:1;
+PRODUCE 'x15:1,x15:1,'m1:1;
+
+TRANSITION ''t30
+CONSUME 'x14:1,'m2:1;
+PRODUCE 'x15:1,'sigma:1,'m2:1;
+
+TRANSITION 't31
+CONSUME 'x15:1,'x151:1,x15:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t31
+CONSUME 'x15:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't32
+CONSUME 'x15:1,x15:1,'m1:1;
+PRODUCE 'x16:1,x16:1,'m1:1;
+
+TRANSITION ''t32
+CONSUME 'x15:1,'m2:1;
+PRODUCE 'x16:1,'sigma:1,'m2:1;
+
+TRANSITION 't33
+CONSUME 'x16:1,'x151:1,x16:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t33
+CONSUME 'x16:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't34
+CONSUME 'x16:1,x16:1,'m1:1;
+PRODUCE 'x17:1,x17:1,'m1:1;
+
+TRANSITION ''t34
+CONSUME 'x16:1,'m2:1;
+PRODUCE 'x17:1,'sigma:1,'m2:1;
+
+TRANSITION 't35
+CONSUME 'x17:1,'x151:1,x17:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t35
+CONSUME 'x17:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't36
+CONSUME 'x17:1,x17:1,'m1:1;
+PRODUCE 'x18:1,x18:1,'m1:1;
+
+TRANSITION ''t36
+CONSUME 'x17:1,'m2:1;
+PRODUCE 'x18:1,'sigma:1,'m2:1;
+
+TRANSITION 't37
+CONSUME 'x18:1,'x151:1,x18:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t37
+CONSUME 'x18:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't38
+CONSUME 'x18:1,x18:1,'m1:1;
+PRODUCE 'x19:1,x19:1,'m1:1;
+
+TRANSITION ''t38
+CONSUME 'x18:1,'m2:1;
+PRODUCE 'x19:1,'sigma:1,'m2:1;
+
+TRANSITION 't39
+CONSUME 'x19:1,'x151:1,x19:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t39
+CONSUME 'x19:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't40
+CONSUME 'x19:1,x19:1,'m1:1;
+PRODUCE 'x20:1,x20:1,'m1:1;
+
+TRANSITION ''t40
+CONSUME 'x19:1,'m2:1;
+PRODUCE 'x20:1,'sigma:1,'m2:1;
+
+TRANSITION 't41
+CONSUME 'x20:1,'x151:1,x20:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t41
+CONSUME 'x20:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't42
+CONSUME 'x20:1,x20:1,'m1:1;
+PRODUCE 'x21:1,x21:1,'m1:1;
+
+TRANSITION ''t42
+CONSUME 'x20:1,'m2:1;
+PRODUCE 'x21:1,'sigma:1,'m2:1;
+
+TRANSITION 't43
+CONSUME 'x21:1,'x151:1,x21:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t43
+CONSUME 'x21:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't44
+CONSUME 'x21:1,x21:1,'m1:1;
+PRODUCE 'x22:1,x22:1,'m1:1;
+
+TRANSITION ''t44
+CONSUME 'x21:1,'m2:1;
+PRODUCE 'x22:1,'sigma:1,'m2:1;
+
+TRANSITION 't45
+CONSUME 'x22:1,'x151:1,x22:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t45
+CONSUME 'x22:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't46
+CONSUME 'x22:1,x22:1,'m1:1;
+PRODUCE 'x23:1,x23:1,'m1:1;
+
+TRANSITION ''t46
+CONSUME 'x22:1,'m2:1;
+PRODUCE 'x23:1,'sigma:1,'m2:1;
+
+TRANSITION 't47
+CONSUME 'x23:1,'x151:1,x23:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t47
+CONSUME 'x23:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't48
+CONSUME 'x23:1,x23:1,'m1:1;
+PRODUCE 'x24:1,x24:1,'m1:1;
+
+TRANSITION ''t48
+CONSUME 'x23:1,'m2:1;
+PRODUCE 'x24:1,'sigma:1,'m2:1;
+
+TRANSITION 't49
+CONSUME 'x24:1,'x151:1,x24:1,x151:1,'m1:1;
+PRODUCE 'x0:1,'x152:1,x0:1,x152:1,'m1:1;
+
+TRANSITION ''t49
+CONSUME 'x24:1,'x151:1,'m2:1;
+PRODUCE 'x0:1,'x152:1,'sigma:1,'m2:1;
+
+TRANSITION 't50
+CONSUME 'x24:1,x24:1,'m1:1;
+PRODUCE 'x25:1,x25:1,'m1:1;