[     0.001] (INFO) [37mWrite simplified version of 'old' to output_1/old_Main_simplified.st[0m [[33mmodularization.kt:251[0m]
[     0.029] (INFO) [37mMaintain frames in old[0m [[33mmodularization.kt:254[0m]
[     0.167] (INFO) [37mWrite complete SMV file of 'old' to output_1/old_Main_simplified.smv[0m [[33mmodularization.kt:259[0m]
[     0.219] (INFO) [37mWrite simplified version of 'new' to output_1/new_Main_simplified.st[0m [[33mmodularization.kt:251[0m]
[     0.225] (INFO) [37mMaintain frames in new[0m [[33mmodularization.kt:254[0m]
[     0.313] (INFO) [37mWrite complete SMV file of 'new' to output_1/new_Main_simplified.smv[0m [[33mmodularization.kt:259[0m]
[     0.335] (INFO) [37mTop level relation: Sensor_CraneDown = Sensor_CraneDown & Sensor_CraneOnConveyor = Sensor_CraneOnConveyor & Sensor_CraneOnMagazin = Sensor_CraneOnMagazin & Sensor_CranePosition = Sensor_CranePosition & Sensor_CraneSucked = Sensor_CraneSucked & Sensor_CraneUp = Sensor_CraneUp & Sensor_MagazinEmergencyStop = Sensor_MagazinEmergencyStop & Sensor_MagazinSwitchManuellAutomatic = Sensor_MagazinSwitchManuellAutomatic & Sensor_SliderMovedOut = Sensor_SliderMovedOut & Sensor_SliderNotMovedOut = Sensor_SliderNotMovedOut & Sensor_StartButtonMagazin = Sensor_StartButtonMagazin & Sensor_WorkpieceReady = Sensor_WorkpieceReady[0m [[33mapp.kt:89[0m]
[     0.335] (INFO) [37mTop level conditon: SBooleanLiteral(value=true)[0m [[33mapp.kt:90[0m]
[     0.335] (INFO) [37mProof for perfect equality? true[0m [[33mapp.kt:91[0m]
[     0.335] (INFO) [37mOnly equalities? true[0m [[33mapp.kt:92[0m]
[     0.340] (INFO) [37mCall sites for the old program: Main[0m [[33mmodularization.kt:195[0m]
[     0.340] (INFO) [37mMain.Mag.0 in line @106:8, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.340] (INFO) [37mMain.Crane.0 in line @264:8, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.341] (INFO) [37mMain.Crane.TimeDelay_Timer.0 in line @384:24, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.341] (INFO) [37mCall sites for the new program: Main[0m [[33mmodularization.kt:199[0m]
[     0.341] (INFO) [37mMain.Mag.0 in line @117:8, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.341] (INFO) [37mMain.Crane.0 in line @281:8, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.341] (INFO) [37mMain.Crane.TimeDelay_Timer.0 in line @402:24, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.342] (INFO) [37mMatched Main.Crane.0 to Main.Crane.0[0m [[33mmodularization.kt:206[0m]
[     0.342] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:207[0m]
[     0.343] (INFO) [37m	Input-Relation: old.Crane$CraneDown = new.Crane$CraneDown & old.Crane$CraneOnConveyor = new.Crane$CraneOnConveyor & old.Crane$CraneOnMagazin = new.Crane$CraneOnMagazin & old.Crane$CraneSucked = new.Crane$CraneSucked & old.Crane$CraneUp = new.Crane$CraneUp & old.Crane$SFCReset = new.Crane$SFCReset & old.Crane$SliderMovedOut = new.Crane$SliderMovedOut & old.Crane$SliderNotMovedOut = new.Crane$SliderNotMovedOut & old.Crane$StartButtonMagazin = new.Crane$StartButtonMagazin & old.Crane$StartVar = new.Crane$StartVar & old.Crane$WorkpieceReady = new.Crane$WorkpieceReady[0m [[33mmodularization.kt:208[0m]
[     0.343] (INFO) [37m	Output-Relation: old.Crane$CraneLower = new.Crane$CraneLower & old.Crane$CraneTurnClockwise = new.Crane$CraneTurnClockwise & old.Crane$CraneTurnCounterclockwise = new.Crane$CraneTurnCounterclockwise & old.Crane$MagazinVacuumOff = new.Crane$MagazinVacuumOff & old.Crane$MagazinVacuumOn = new.Crane$MagazinVacuumOn & old.Crane$StartCommandCrane = new.Crane$StartCommandCrane[0m [[33mmodularization.kt:209[0m]
[     0.343] (INFO) [37mMatched Main.Mag.0 to Main.Mag.0[0m [[33mmodularization.kt:206[0m]
[     0.343] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:207[0m]
[     0.344] (INFO) [37m	Input-Relation: old.Mag$CraneDown = new.Mag$CraneDown & old.Mag$CraneOnConveyor = new.Mag$CraneOnConveyor & old.Mag$CraneOnMagazin = new.Mag$CraneOnMagazin & old.Mag$CraneSucked = new.Mag$CraneSucked & old.Mag$CraneUp = new.Mag$CraneUp & old.Mag$SFCReset = new.Mag$SFCReset & old.Mag$SliderMovedOut = new.Mag$SliderMovedOut & old.Mag$SliderNotMovedOut = new.Mag$SliderNotMovedOut & old.Mag$StartButtonMagazin = new.Mag$StartButtonMagazin & old.Mag$StartVar = new.Mag$StartVar & old.Mag$WorkpieceReady = new.Mag$WorkpieceReady[0m [[33mmodularization.kt:208[0m]
[     0.344] (INFO) [37m	Output-Relation: old.Mag$MagazinGreenLamp = new.Mag$MagazinGreenLamp & old.Mag$MagazinSlider = new.Mag$MagazinSlider & old.Mag$StartCommandMagazin = new.Mag$StartCommandMagazin[0m [[33mmodularization.kt:209[0m]
[     0.344] (INFO) [37mMatched Main.Crane.TimeDelay_Timer.0 to Main.Crane.TimeDelay_Timer.0[0m [[33mmodularization.kt:206[0m]
[     0.344] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:207[0m]
[     0.345] (INFO) [37m	Input-Relation: old.Crane$TimeDelay_Timer$IN = new.Crane$TimeDelay_Timer$IN & old.Crane$TimeDelay_Timer$PT = new.Crane$TimeDelay_Timer$PT[0m [[33mmodularization.kt:208[0m]
[     0.345] (INFO) [37m	Output-Relation: old.Crane$TimeDelay_Timer$ET = new.Crane$TimeDelay_Timer$ET & old.Crane$TimeDelay_Timer$Q = new.Crane$TimeDelay_Timer$Q[0m [[33mmodularization.kt:209[0m]
[     0.345] (INFO) [37mOutput folder: output_1[0m [[33mapp.kt:118[0m]
[     0.345] (INFO) [37mStart with the proof[0m [[33mapp.kt:119[0m]
[     0.352] (INFO) [37mproofEquivalence(Main,Main):  Main.0: (LoC:357) (Vars: [41] (12) => (11))[0m [[33mstrategy.kt:71[0m]
[     0.357] (INFO) [37mproofEquivalence(Main,Main):  Main.0: (LoC:387) (Vars: [42] (13) => (17))[0m [[33mstrategy.kt:72[0m]
[     0.358] (INFO) [37mcheckCache(Main,Main):  Skipped because `disableCheckCache` is set[0m [[33mstrategy.kt:106[0m]
[     0.358] (INFO) [37mproofBodyEquivalenceSource(Main,Main):  Skipped because `disableProofBodyEquivalenceSource` is set[0m [[33mstrategy.kt:329[0m]
[     0.358] (INFO) [37mproofBodyEquivalenceSSA(Main,Main):  Skipped because `disableProofBodyEquivalenceSSA` is set[0m [[33mstrategy.kt:349[0m]
[     0.359] (INFO) [37mproofBodyEquivalenceSMT(Main,Main):  Skipped because `disableProofBodyEquivalenceSMT` is set[0m [[33mstrategy.kt:374[0m]
[     0.359] (INFO) [37mproofBodyEquivalenceWithAbstraction(Main,Main):  Skipped because `disableProofBodyEquivalenceWithAbstraction` is set[0m [[33mstrategy.kt:202[0m]
[     0.422] (INFO) [37mproofBodyEquivalenceClassic(Main,Main):  Starting proof: output_1/Main_Main.smv, output_1/Main_Main.log[0m [[33mstrategy.kt:163[0m]
[     0.455] (INFO) [37mrunNuXmv: Run solver on output_1/Main_Main.smv[0m [[33mstrategy.kt:486[0m]
[     0.456] (INFO) [37mCreate nuXmv command file `output_1/ic3.xmv'[0m [[33mstrategy.kt:505[0m]
[     0.456] (INFO) [37m/home/weigl/share/nuXmv-1.1.1-Linux/bin/nuXmv -int /home/weigl/work/verifaps-lib/aps-rvt/examples/ppumod/01_02/output_1/Main_Main.smv[0m [[33mstrategy.kt:819[0m]
[    10.166] (INFO) [37mrunNuXmv: Solver finished for output_1/Main_Main.smv with edu.kit.iti.formal.smv.NuXMVOutput$Verified@1583741e[0m [[33mstrategy.kt:490[0m]
[    10.167] (INFO) [37mproofBodyEquivalenceClassic(Main,Main):  Equality proven[0m [[33mstrategy.kt:168[0m]
[    10.167] (INFO) [37mupdateCache(Main,Main):  Skipped because `disableUpdateCache` is set[0m [[33mstrategy.kt:125[0m]
[    10.168] (INFO) [37mproofEquivalence(Main,Main):  Timings: {cache=1, cmc=9808, mod=0, smt=1, src=0, ssa=0}[0m [[33mstrategy.kt:96[0m]
[    10.168] (INFO) [37mProof result: true[0m [[33mmodularization.kt:217[0m]
