learn_three_twenty.log

Start learning of no-invariant TA
[2023-08-18 18:25:20.038941] [0x00007ff84b102640] [info]    Target DTA
digraph G {
        loc0 [init=true, match=false]
        loc1 [init=false, match=true]
        loc0->loc1 [label="b", guard="{x1 <= 20, x1 >= 20}", reset="{x0 := 0}"]
        loc0->loc0 [label="a", guard="{x0 <= 3, x0 >= 3}", reset="{x0 := 0}"]
}

[2023-08-18 18:25:20.042653] [0x00007ff84b102640] [info]    Complement of the target DTA
digraph G {
        loc0 [init=true, match=true]
        loc1 [init=false, match=false]
        loc2 [init=false, match=true]
        loc0->loc0 [label="a", guard="{x0 <= 3, x0 >= 3}", reset="{x0 := 0}"]
        loc0->loc2 [label="a", guard="{x0 > 3}"]
        loc0->loc2 [label="a", guard="{x0 < 3}"]
        loc0->loc1 [label="b", guard="{x1 <= 20, x1 >= 20}", reset="{x0 := 0}"]
        loc0->loc2 [label="b", guard="{x1 > 20}"]
        loc0->loc2 [label="b", guard="{x1 < 20}"]
        loc1->loc2 [label="b"]
        loc1->loc2 [label="a"]
        loc2->loc2 [label="b"]
        loc2->loc2 [label="a"]
}

[2023-08-18 18:25:20.042892] [0x00007ff84b102640] [info]    Start Learning!!
[2023-08-18 18:25:20.043225] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.043268] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.043622] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.048923] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.048983] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.049009] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.054302] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.054331] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.054346] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.059157] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.059256] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.059307] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.065361] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.065400] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.065422] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.070186] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.070217] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.070238] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.075470] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.075530] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.075559] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.081669] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.081705] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.081726] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.086744] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.086780] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.086802] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.094499] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.094578] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.094624] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.100649] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.100679] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.100700] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.107347] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.107382] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.107403] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.114814] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.114850] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.114874] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.126061] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.126089] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.126107] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.133497] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.133532] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.133555] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.140823] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.140854] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.140875] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.151052] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.151089] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.151145] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.162580] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.162698] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.162811] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.172428] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.172459] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.172480] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.185245] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.185284] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:20.185307] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 20 b 0
[2023-08-18 18:25:20.203104] [0x00007ff84b102640] [info]    There are 6 dead states in the zone graph
[2023-08-18 18:25:20.203229] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
        loc0 [init=true, match=false]
        loc1 [init=false, match=true]
        loc0->loc0 [label="a", guard="{x0 >= 3, x0 <= 3}", reset="{x0 := 3}"]
        loc0->loc1 [label="b", guard="{x0 >= 20, x0 <= 20}", reset="{x1 := 0}"]
}

[2023-08-18 18:25:20.203292] [0x00007ff84b102640] [info]    There are 2 redundant states
[2023-08-18 18:25:20.203306] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.203978] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 0 a 17 b 0
[2023-08-18 18:25:20.389639] [0x00007ff84b102640] [info]    There are 117 dead states in the zone graph
[2023-08-18 18:25:20.390055] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
        loc0 [init=true, match=false]
        loc1 [init=false, match=false]
        loc2 [init=false, match=true]
        loc0->loc2 [label="b", guard="{x0 >= 20, x0 <= 20}", reset="{x1 := 0}"]
        loc0->loc1 [label="a", guard="{x0 >= 3, x0 <= 3}", reset="{x1 := 0}"]
        loc1->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17}", reset="{x0 := 20, x1 := 0}"]
        loc1->loc0 [label="a", guard="{x0 >= 6, x0 <= 6, x1 >= 3, x1 <= 3}", reset="{x0 := 6}"]
}

[2023-08-18 18:25:20.390151] [0x00007ff84b102640] [info]    There are 3 redundant states
[2023-08-18 18:25:20.390168] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.390325] [0x00007ff84b102640] [info]    There are 3 redundant states
[2023-08-18 18:25:20.390340] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.390545] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 11 b 0
[2023-08-18 18:25:20.545153] [0x00007ff84b102640] [info]    There are 486 dead states in the zone graph
[2023-08-18 18:25:20.547330] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
        loc0 [init=true, match=false]
        loc1 [init=false, match=false]
        loc2 [init=false, match=true]
        loc3 [init=false, match=false]
        loc0->loc2 [label="b", guard="{x0 >= 20, x0 <= 20}", reset="{x1 := 0}"]
        loc0->loc1 [label="a", guard="{x0 >= 3, x0 <= 3}", reset="{x1 := 0}"]
        loc1->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17}", reset="{x0 := 20, x1 := 0}"]
        loc1->loc3 [label="a", guard="{x0 >= 6, x0 <= 6, x1 >= 3, x1 <= 3}", reset="{x2 := 0}"]
        loc3->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14}", reset="{x0 := 20, x1 := 0}"]
        loc3->loc1 [label="a", guard="{x0 >= 9, x0 <= 9, x1 >= 6, x1 <= 6, x2 >= 3, x2 <= 3}", reset="{x0 := 9, x1 := 6}"]
}

[2023-08-18 18:25:20.547437] [0x00007ff84b102640] [info]    There are 5 redundant states
[2023-08-18 18:25:20.547456] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.547675] [0x00007ff84b102640] [info]    There are 4 redundant states
[2023-08-18 18:25:20.547694] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.547960] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 8 b 0
[2023-08-18 18:25:20.792739] [0x00007ff84b102640] [info]    There are 817 dead states in the zone graph
[2023-08-18 18:25:20.794451] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
        loc0 [init=true, match=false]
        loc1 [init=false, match=false]
        loc2 [init=false, match=true]
        loc3 [init=false, match=false]
        loc4 [init=false, match=false]
        loc0->loc2 [label="b", guard="{x0 >= 20, x0 <= 20}", reset="{x1 := 0}"]
        loc0->loc1 [label="a", guard="{x0 >= 3, x0 <= 3}", reset="{x1 := 0}"]
        loc1->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17}", reset="{x0 := 20, x1 := 0}"]
        loc1->loc3 [label="a", guard="{x0 >= 6, x0 <= 6, x1 >= 3, x1 <= 3}", reset="{x2 := 0}"]
        loc3->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14}", reset="{x0 := 20, x1 := 0}"]
        loc3->loc4 [label="a", guard="{x0 >= 9, x0 <= 9, x1 >= 6, x1 <= 6, x2 >= 3, x2 <= 3}", reset="{x3 := 0}"]
        loc4->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14, x3 >= 11, x3 <= 11}", reset="{x0 := 20, x1 := 0}"]
        loc4->loc3 [label="a", guard="{x0 >= 12, x0 <= 12, x1 >= 9, x1 <= 9, x2 >= 6, x2 <= 6, x3 >= 3, x3 <= 3}", reset="{x0 := 12, x1 := 9, x2 := 6}"]
}

[2023-08-18 18:25:20.794676] [0x00007ff84b102640] [info]    There are 6 redundant states
[2023-08-18 18:25:20.794694] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.794942] [0x00007ff84b102640] [info]    There are 5 redundant states
[2023-08-18 18:25:20.794962] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:20.795357] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 5 b 0
[2023-08-18 18:25:21.059476] [0x00007ff84b102640] [info]    There are 1063 dead states in the zone graph
[2023-08-18 18:25:21.067492] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
        loc0 [init=true, match=false]
        loc1 [init=false, match=false]
        loc2 [init=false, match=true]
        loc3 [init=false, match=false]
        loc4 [init=false, match=false]
        loc5 [init=false, match=false]
        loc0->loc2 [label="b", guard="{x0 >= 20, x0 <= 20}", reset="{x1 := 0}"]
        loc0->loc1 [label="a", guard="{x0 >= 3, x0 <= 3}", reset="{x1 := 0}"]
        loc1->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17}", reset="{x0 := 20, x1 := 0}"]
        loc1->loc3 [label="a", guard="{x0 >= 6, x0 <= 6, x1 >= 3, x1 <= 3}", reset="{x2 := 0}"]
        loc3->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14}", reset="{x0 := 20, x1 := 0}"]
        loc3->loc4 [label="a", guard="{x0 >= 9, x0 <= 9, x1 >= 6, x1 <= 6, x2 >= 3, x2 <= 3}", reset="{x3 := 0}"]
        loc4->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14, x3 >= 11, x3 <= 11}", reset="{x0 := 20, x1 := 0}"]
        loc4->loc5 [label="a", guard="{x0 >= 12, x0 <= 12, x1 >= 9, x1 <= 9, x2 >= 6, x2 <= 6, x3 >= 3, x3 <= 3}", reset="{x4 := 0}"]
        loc5->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14, x3 >= 11, x3 <= 11, x4 >= 8, x4 <= 8}", reset="{x0 := 20, x1 := 0}"]
        loc5->loc4 [label="a", guard="{x0 >= 15, x0 <= 15, x1 >= 12, x1 <= 12, x2 >= 9, x2 <= 9, x3 >= 6, x3 <= 6, x4 >= 3, x4 <= 3}", reset="{x0 := 15, x1 := 12, x2 := 9, x3 := 6}"]
}

[2023-08-18 18:25:21.067780] [0x00007ff84b102640] [info]    There are 7 redundant states
[2023-08-18 18:25:21.067834] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:21.068445] [0x00007ff84b102640] [info]    There are 6 redundant states
[2023-08-18 18:25:21.068488] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:21.069162] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.431494] [0x00007ff84b102640] [info]    There are 1241 dead states in the zone graph
[2023-08-18 18:25:21.434460] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
        loc0 [init=true, match=false]
        loc1 [init=false, match=false]
        loc2 [init=false, match=true]
        loc3 [init=false, match=false]
        loc4 [init=false, match=false]
        loc5 [init=false, match=false]
        loc6 [init=false, match=false]
        loc0->loc2 [label="b", guard="{x0 >= 20, x0 <= 20}", reset="{x1 := 0}"]
        loc0->loc1 [label="a", guard="{x0 >= 3, x0 <= 3}", reset="{x1 := 0}"]
        loc1->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17}", reset="{x0 := 20, x1 := 0}"]
        loc1->loc3 [label="a", guard="{x0 >= 6, x0 <= 6, x1 >= 3, x1 <= 3}", reset="{x2 := 0}"]
        loc3->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14}", reset="{x0 := 20, x1 := 0}"]
        loc3->loc4 [label="a", guard="{x0 >= 9, x0 <= 9, x1 >= 6, x1 <= 6, x2 >= 3, x2 <= 3}", reset="{x3 := 0}"]
        loc4->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14, x3 >= 11, x3 <= 11}", reset="{x0 := 20, x1 := 0}"]
        loc4->loc5 [label="a", guard="{x0 >= 12, x0 <= 12, x1 >= 9, x1 <= 9, x2 >= 6, x2 <= 6, x3 >= 3, x3 <= 3}", reset="{x4 := 0}"]
        loc5->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14, x3 >= 11, x3 <= 11, x4 >= 8, x4 <= 8}", reset="{x0 := 20, x1 := 0}"]
        loc5->loc6 [label="a", guard="{x0 >= 15, x0 <= 15, x1 >= 12, x1 <= 12, x2 >= 9, x2 <= 9, x3 >= 6, x3 <= 6, x4 >= 3, x4 <= 3}", reset="{x5 := 0}"]
        loc6->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14, x3 >= 11, x3 <= 11, x4 >= 8, x4 <= 8, x5 >= 5, x5 <= 5}", reset="{x0 := 20, x1 := 0}"]
        loc6->loc5 [label="a", guard="{x0 >= 18, x0 <= 18, x1 >= 15, x1 <= 15, x2 >= 12, x2 <= 12, x3 >= 9, x3 <= 9, x4 >= 6, x4 <= 6, x5 >= 3, x5 <= 3}", reset="{x0 := 18, x1 := 15, x2 := 12, x3 := 9, x4 := 6}"]
}

[2023-08-18 18:25:21.434786] [0x00007ff84b102640] [info]    There are 8 redundant states
[2023-08-18 18:25:21.434824] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:21.435442] [0x00007ff84b102640] [info]    There are 7 redundant states
[2023-08-18 18:25:21.435467] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:21.436406] [0x00007ff84b102640] [info]    Learning Finished!!
[2023-08-18 18:25:21.436510] [0x00007ff84b102640] [info]    The learned DTA is as follows
digraph G {
        loc0 [init=true, match=false]
        loc1 [init=false, match=false]
        loc2 [init=false, match=true]
        loc3 [init=false, match=false]
        loc4 [init=false, match=false]
        loc5 [init=false, match=false]
        loc6 [init=false, match=false]
        loc0->loc2 [label="b", guard="{x0 >= 20, x0 <= 20}", reset="{x1 := 0}"]
        loc0->loc1 [label="a", guard="{x0 >= 3, x0 <= 3}", reset="{x1 := 0}"]
        loc1->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17}", reset="{x0 := 20, x1 := 0}"]
        loc1->loc3 [label="a", guard="{x0 >= 6, x0 <= 6, x1 >= 3, x1 <= 3}", reset="{x2 := 0}"]
        loc3->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14}", reset="{x0 := 20, x1 := 0}"]
        loc3->loc4 [label="a", guard="{x0 >= 9, x0 <= 9, x1 >= 6, x1 <= 6, x2 >= 3, x2 <= 3}", reset="{x3 := 0}"]
        loc4->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14, x3 >= 11, x3 <= 11}", reset="{x0 := 20, x1 := 0}"]
        loc4->loc5 [label="a", guard="{x0 >= 12, x0 <= 12, x1 >= 9, x1 <= 9, x2 >= 6, x2 <= 6, x3 >= 3, x3 <= 3}", reset="{x4 := 0}"]
        loc5->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14, x3 >= 11, x3 <= 11, x4 >= 8, x4 <= 8}", reset="{x0 := 20, x1 := 0}"]
        loc5->loc6 [label="a", guard="{x0 >= 15, x0 <= 15, x1 >= 12, x1 <= 12, x2 >= 9, x2 <= 9, x3 >= 6, x3 <= 6, x4 >= 3, x4 <= 3}", reset="{x5 := 0}"]
        loc6->loc2 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14, x3 >= 11, x3 <= 11, x4 >= 8, x4 <= 8, x5 >= 5, x5 <= 5}", reset="{x0 := 20, x1 := 0}"]
        loc6->loc5 [label="a", guard="{x0 >= 18, x0 <= 18, x1 >= 15, x1 <= 15, x2 >= 12, x2 <= 12, x3 >= 9, x3 <= 9, x4 >= 6, x4 <= 6, x5 >= 3, x5 <= 3}", reset="{x0 := 18, x1 := 15, x2 := 12, x3 := 9, x4 := 6}"]
}

|P| = 169
|ext(P)| = 339
|S| = 77
Number of symbolic membership queries: 43330
Number of symbolic membership queries (with cache): 27256
Number of membership queries: 40315
Number of membership queries (with cache): 37619
Number of equivalence queries: 26
Number of equivalence queries (with cache): 7
[2023-08-18 18:25:21.436739] [0x00007ff84b102640] [info]    Execution Time: 1393 [ms]
Start learning of invariant-at-transition TA
[2023-08-18 18:25:21.515311] [0x00007ff84b102640] [info]    Target DTA
digraph G {
        loc0 [init=true, match=false]
        loc1 [init=false, match=true]
        loc0->loc1 [label="b", guard="{x0 <= 3, x1 <= 20, x1 >= 20}", reset="{x0 := 0}"]
        loc0->loc0 [label="a", guard="{x0 <= 3, x0 >= 3, x1 <= 20}", reset="{x0 := 0}"]
}

[2023-08-18 18:25:21.515616] [0x00007ff84b102640] [info]    Complement of the target DTA
digraph G {
        loc0 [init=true, match=true]
        loc1 [init=false, match=false]
        loc2 [init=false, match=true]
        loc0->loc0 [label="a", guard="{x0 <= 3, x0 >= 3, x1 <= 20}", reset="{x0 := 0}"]
        loc0->loc2 [label="a", guard="{x0 > 3}"]
        loc0->loc2 [label="a", guard="{x0 < 3}"]
        loc0->loc2 [label="a", guard="{x1 > 20}"]
        loc0->loc1 [label="b", guard="{x0 <= 3, x1 <= 20, x1 >= 20}", reset="{x0 := 0}"]
        loc0->loc2 [label="b", guard="{x0 > 3}"]
        loc0->loc2 [label="b", guard="{x1 > 20}"]
        loc0->loc2 [label="b", guard="{x1 < 20}"]
        loc1->loc2 [label="b"]
        loc1->loc2 [label="a"]
        loc2->loc2 [label="b"]
        loc2->loc2 [label="a"]
}

[2023-08-18 18:25:21.515679] [0x00007ff84b102640] [info]    Start Learning!!
[2023-08-18 18:25:21.515729] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:21.515742] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.515879] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.522908] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:21.522986] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.523035] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.530578] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:21.530615] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.530636] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.538835] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:21.538864] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.538890] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.548189] [0x00007ff84b102640] [info]    There are 2 dead states
[2023-08-18 18:25:21.548219] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.548236] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.557139] [0x00007ff84b102640] [info]    There are 2 dead states
[2023-08-18 18:25:21.557170] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.557189] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.565495] [0x00007ff84b102640] [info]    There are 2 dead states
[2023-08-18 18:25:21.565585] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.565612] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.578533] [0x00007ff84b102640] [info]    There are 3 dead states
[2023-08-18 18:25:21.578564] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.578582] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.591009] [0x00007ff84b102640] [info]    There are 3 dead states
[2023-08-18 18:25:21.591042] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.591060] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.600905] [0x00007ff84b102640] [info]    There are 3 dead states
[2023-08-18 18:25:21.600939] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.600957] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.616470] [0x00007ff84b102640] [info]    There are 4 dead states
[2023-08-18 18:25:21.616503] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.616521] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.630743] [0x00007ff84b102640] [info]    There are 4 dead states
[2023-08-18 18:25:21.630774] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.630792] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.642917] [0x00007ff84b102640] [info]    There are 4 dead states
[2023-08-18 18:25:21.642953] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.642971] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.679648] [0x00007ff84b102640] [info]    There are 5 dead states
[2023-08-18 18:25:21.679742] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.679797] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.721132] [0x00007ff84b102640] [info]    There are 5 dead states
[2023-08-18 18:25:21.721246] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.721312] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.757915] [0x00007ff84b102640] [info]    There are 5 dead states
[2023-08-18 18:25:21.758106] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.758174] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.788524] [0x00007ff84b102640] [info]    There are 6 dead states
[2023-08-18 18:25:21.788604] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.788640] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.816627] [0x00007ff84b102640] [info]    There are 6 dead states
[2023-08-18 18:25:21.816662] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.816682] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.836222] [0x00007ff84b102640] [info]    There are 6 dead states
[2023-08-18 18:25:21.836261] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.836280] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:21.892605] [0x00007ff84b102640] [info]    There are 7 dead states
[2023-08-18 18:25:21.892740] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
}

[2023-08-18 18:25:21.892830] [0x00007ff84b102640] [info]    Equivalence oracle returned a counter example: 3 a 3 a 3 a 3 a 3 a 3 a 2 b 0
[2023-08-18 18:25:22.007379] [0x00007ff84b102640] [info]    There are 167 dead states in the zone graph
[2023-08-18 18:25:22.008193] [0x00007ff84b102640] [info]    The learner generated a hypothesis
digraph G {
        loc0 [init=true, match=false]
        loc1 [init=false, match=false]
        loc2 [init=false, match=false]
        loc3 [init=false, match=false]
        loc4 [init=false, match=false]
        loc5 [init=false, match=false]
        loc6 [init=false, match=false]
        loc7 [init=false, match=true]
        loc0->loc1 [label="a", guard="{x0 >= 3, x0 <= 3}", reset="{x1 := 0}"]
        loc1->loc2 [label="a", guard="{x0 >= 6, x0 <= 6, x1 >= 3, x1 <= 3}", reset="{x2 := 0}"]
        loc2->loc3 [label="a", guard="{x0 >= 9, x0 <= 9, x1 >= 6, x1 <= 6, x2 >= 3, x2 <= 3}", reset="{x3 := 0}"]
        loc3->loc4 [label="a", guard="{x0 >= 12, x0 <= 12, x1 >= 9, x1 <= 9, x2 >= 6, x2 <= 6, x3 >= 3, x3 <= 3}", reset="{x4 := 0}"]
        loc4->loc5 [label="a", guard="{x0 >= 15, x0 <= 15, x1 >= 12, x1 <= 12, x2 >= 9, x2 <= 9, x3 >= 6, x3 <= 6, x4 >= 3, x4 <= 3}", reset="{x5 := 0}"]
        loc5->loc6 [label="a", guard="{x0 >= 18, x0 <= 18, x1 >= 15, x1 <= 15, x2 >= 12, x2 <= 12, x3 >= 9, x3 <= 9, x4 >= 6, x4 <= 6, x5 >= 3, x5 <= 3}", reset="{x6 := 0}"]
        loc6->loc7 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14, x3 >= 11, x3 <= 11, x4 >= 8, x4 <= 8, x5 >= 5, x5 <= 5, x6 >= 2, x6 <= 2}", reset="{x7 := 0}"]
}

[2023-08-18 18:25:22.008656] [0x00007ff84b102640] [info]    There are 9 redundant states
[2023-08-18 18:25:22.008693] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:22.009299] [0x00007ff84b102640] [info]    There are 8 redundant states
[2023-08-18 18:25:22.009325] [0x00007ff84b102640] [info]    There are 1 dead states
[2023-08-18 18:25:22.009965] [0x00007ff84b102640] [info]    Learning Finished!!
[2023-08-18 18:25:22.010045] [0x00007ff84b102640] [info]    The learned DTA is as follows
digraph G {
        loc0 [init=true, match=false]
        loc1 [init=false, match=false]
        loc2 [init=false, match=false]
        loc3 [init=false, match=false]
        loc4 [init=false, match=false]
        loc5 [init=false, match=false]
        loc6 [init=false, match=false]
        loc7 [init=false, match=true]
        loc0->loc1 [label="a", guard="{x0 >= 3, x0 <= 3}", reset="{x1 := 0}"]
        loc1->loc2 [label="a", guard="{x0 >= 6, x0 <= 6, x1 >= 3, x1 <= 3}", reset="{x2 := 0}"]
        loc2->loc3 [label="a", guard="{x0 >= 9, x0 <= 9, x1 >= 6, x1 <= 6, x2 >= 3, x2 <= 3}", reset="{x3 := 0}"]
        loc3->loc4 [label="a", guard="{x0 >= 12, x0 <= 12, x1 >= 9, x1 <= 9, x2 >= 6, x2 <= 6, x3 >= 3, x3 <= 3}", reset="{x4 := 0}"]
        loc4->loc5 [label="a", guard="{x0 >= 15, x0 <= 15, x1 >= 12, x1 <= 12, x2 >= 9, x2 <= 9, x3 >= 6, x3 <= 6, x4 >= 3, x4 <= 3}", reset="{x5 := 0}"]
        loc5->loc6 [label="a", guard="{x0 >= 18, x0 <= 18, x1 >= 15, x1 <= 15, x2 >= 12, x2 <= 12, x3 >= 9, x3 <= 9, x4 >= 6, x4 <= 6, x5 >= 3, x5 <= 3}", reset="{x6 := 0}"]
        loc6->loc7 [label="b", guard="{x0 >= 20, x0 <= 20, x1 >= 17, x1 <= 17, x2 >= 14, x2 <= 14, x3 >= 11, x3 <= 11, x4 >= 8, x4 <= 8, x5 >= 5, x5 <= 5, x6 >= 2, x6 <= 2}", reset="{x7 := 0}"]
}

|P| = 62
|ext(P)| = 125
|S| = 48
Number of symbolic membership queries: 10306
Number of symbolic membership queries (with cache): 6564
Number of membership queries: 9622
Number of membership queries (with cache): 8222
Number of equivalence queries: 21
Number of equivalence queries (with cache): 2
[2023-08-18 18:25:22.010200] [0x00007ff84b102640] [info]    Execution Time: 494 [ms]

Process finished with exit code 0