[     0.002] (INFO) [37mWrite simplified version of 'old' to output_1/old_Main_simplified.st[0m [[33mmodularization.kt:253[0m]
[     0.037] (INFO) [37mMaintain frames in old[0m [[33mmodularization.kt:256[0m]
[     0.400] (INFO) [37mWrite complete SMV file of 'old' to output_1/old_Main_simplified.smv[0m [[33mmodularization.kt:261[0m]
[     0.513] (INFO) [37mWrite simplified version of 'new' to output_1/new_Main_simplified.st[0m [[33mmodularization.kt:253[0m]
[     0.518] (INFO) [37mMaintain frames in new[0m [[33mmodularization.kt:256[0m]
[     0.835] (INFO) [37mWrite complete SMV file of 'new' to output_1/new_Main_simplified.smv[0m [[33mmodularization.kt:261[0m]
[     0.928] (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 & Sensor_CranePositionStamp = Sensor_CranePositionStamp & Sensor_CraneSucked = Sensor_CraneSucked & Sensor_CraneUp = Sensor_CraneUp & Sensor_MagazinCapacitiveSensor = Sensor_MagazinCapacitiveSensor & Sensor_MagazinOpticalSensor = Sensor_MagazinOpticalSensor & Sensor_StampEmergencyStop = Sensor_StampEmergencyStop & Sensor_StampLowered = Sensor_StampLowered & Sensor_StampSliderFilled = Sensor_StampSliderFilled & Sensor_StampSliderSensorMovedIn = Sensor_StampSliderSensorMovedIn & Sensor_StampSliderSensorMovedOut = Sensor_StampSliderSensorMovedOut & Sensor_StampStartButton = Sensor_StampStartButton & Sensor_StampSwitchManuellAutomatic = Sensor_StampSwitchManuellAutomatic & Sensor_StampUp = Sensor_StampUp[0m [[33mapp.kt:89[0m]
[     0.928] (INFO) [37mTop level conditon: old.Sensor_MagazinCapacitiveSensor = TRUE[0m [[33mapp.kt:90[0m]
[     0.928] (INFO) [37mProof for perfect equality? false[0m [[33mapp.kt:91[0m]
[     0.928] (INFO) [37mOnly equalities? true[0m [[33mapp.kt:92[0m]
[     0.934] (INFO) [37mCall sites for the old program: Main[0m [[33mmodularization.kt:195[0m]
[     0.934] (INFO) [37mMain.Mag.0 in line @193:8, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.934] (INFO) [37mMain.Crane.0 in line @357:8, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.934] (INFO) [37mMain.Crane.TimeDelay_Timer.0 in line @488:24, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.935] (INFO) [37mMain.Crane.Timer1.0 in line @674:24, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.935] (INFO) [37mMain.Crane.Timer1.1 in line @702:24, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.935] (INFO) [37mMain.Stamp.0 in line @834:8, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.935] (INFO) [37mMain.Stamp.Timer.0 in line @1027:24, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.935] (INFO) [37mMain.Stamp.Timer.1 in line @1059:24, embedded from null[0m [[33mmodularization.kt:197[0m]
[     0.935] (INFO) [37mCall sites for the new program: Main[0m [[33mmodularization.kt:199[0m]
[     0.936] (INFO) [37mMain.Mag.0 in line @193:8, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.936] (INFO) [37mMain.Crane.0 in line @357:8, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.936] (INFO) [37mMain.Crane.TimeDelay_Timer.0 in line @490:24, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.936] (INFO) [37mMain.Crane.Timer1.0 in line @679:24, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.936] (INFO) [37mMain.Crane.Timer1.1 in line @826:24, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.936] (INFO) [37mMain.Stamp.0 in line @958:8, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.936] (INFO) [37mMain.Stamp.Timer.0 in line @1151:24, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.936] (INFO) [37mMain.Stamp.Timer.1 in line @1183:24, embedded from null[0m [[33mmodularization.kt:201[0m]
[     0.937] (INFO) [37mMatched Main.Crane.0 to Main.Crane.0[0m [[33mmodularization.kt:206[0m]
[     0.937] (INFO) [37m	Is perfect?: false[0m [[33mmodularization.kt:207[0m]
[     0.937] (INFO) [37m	Context: old.Crane$MagazinCapacitiveSensor = TRUE[0m [[33mmodularization.kt:208[0m]
[     0.938] (INFO) [37m	Input-Relation: old.Crane$CraneDown = new.Crane$CraneDown & old.Crane$CraneOnConveyor = new.Crane$CraneOnConveyor & old.Crane$CraneOnMagazin = new.Crane$CraneOnMagazin & old.Crane$CranePositionStamp = new.Crane$CranePositionStamp & old.Crane$CraneSucked = new.Crane$CraneSucked & old.Crane$CraneUp = new.Crane$CraneUp & old.Crane$MagazinCapacitiveSensor = new.Crane$MagazinCapacitiveSensor & old.Crane$SFCReset = new.Crane$SFCReset & old.Crane$SliderMovedOut = new.Crane$SliderMovedOut & old.Crane$SliderNotMovedOut = new.Crane$SliderNotMovedOut & old.Crane$StampLowered = new.Crane$StampLowered & old.Crane$StampSliderFilled = new.Crane$StampSliderFilled & old.Crane$StartButtonMagazin = new.Crane$StartButtonMagazin & old.Crane$StartVar = new.Crane$StartVar & old.Crane$WorkpieceReady = new.Crane$WorkpieceReady[0m [[33mmodularization.kt:209[0m]
[     0.938] (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:210[0m]
[     0.938] (INFO) [37mMatched Main.Mag.0 to Main.Mag.0[0m [[33mmodularization.kt:206[0m]
[     0.938] (INFO) [37m	Is perfect?: true[0m [[33mmodularization.kt:207[0m]
[     0.938] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:208[0m]
[     0.938] (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:209[0m]
[     0.939] (INFO) [37m	Output-Relation: old.Mag$CraneLower = new.Mag$CraneLower & old.Mag$CraneTurnClockwise = new.Mag$CraneTurnClockwise & old.Mag$CraneTurnCounterclockwise = new.Mag$CraneTurnCounterclockwise & old.Mag$MagazinGreenLamp = new.Mag$MagazinGreenLamp & old.Mag$MagazinSlider = new.Mag$MagazinSlider & old.Mag$MagazinVacuumOff = new.Mag$MagazinVacuumOff & old.Mag$MagazinVacuumOn = new.Mag$MagazinVacuumOn & old.Mag$MagazinWhiteLamp = new.Mag$MagazinWhiteLamp & old.Mag$StartCommandMagazin = new.Mag$StartCommandMagazin[0m [[33mmodularization.kt:210[0m]
[     0.939] (INFO) [37mMatched Main.Stamp.Timer.0 to Main.Stamp.Timer.0[0m [[33mmodularization.kt:206[0m]
[     0.939] (INFO) [37m	Is perfect?: true[0m [[33mmodularization.kt:207[0m]
[     0.939] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:208[0m]
[     0.939] (INFO) [37m	Input-Relation: old.Stamp$Timer$IN = new.Stamp$Timer$IN & old.Stamp$Timer$PT = new.Stamp$Timer$PT[0m [[33mmodularization.kt:209[0m]
[     0.939] (INFO) [37m	Output-Relation: old.Stamp$Timer$ET = new.Stamp$Timer$ET & old.Stamp$Timer$Q = new.Stamp$Timer$Q[0m [[33mmodularization.kt:210[0m]
[     0.939] (INFO) [37mMatched Main.Crane.Timer1.0 to Main.Crane.Timer1.0[0m [[33mmodularization.kt:206[0m]
[     0.939] (INFO) [37m	Is perfect?: true[0m [[33mmodularization.kt:207[0m]
[     0.940] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:208[0m]
[     0.940] (INFO) [37m	Input-Relation: old.Crane$Timer1$IN = new.Crane$Timer1$IN & old.Crane$Timer1$PT = new.Crane$Timer1$PT[0m [[33mmodularization.kt:209[0m]
[     0.940] (INFO) [37m	Output-Relation: old.Crane$Timer1$ET = new.Crane$Timer1$ET & old.Crane$Timer1$Q = new.Crane$Timer1$Q[0m [[33mmodularization.kt:210[0m]
[     0.940] (INFO) [37mMatched Main.Stamp.0 to Main.Stamp.0[0m [[33mmodularization.kt:206[0m]
[     0.940] (INFO) [37m	Is perfect?: true[0m [[33mmodularization.kt:207[0m]
[     0.940] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:208[0m]
[     0.941] (INFO) [37m	Input-Relation: old.Stamp$CraneDown = new.Stamp$CraneDown & old.Stamp$CraneOnConveyor = new.Stamp$CraneOnConveyor & old.Stamp$CranePositionStamp = new.Stamp$CranePositionStamp & old.Stamp$CraneSucked = new.Stamp$CraneSucked & old.Stamp$CraneUp = new.Stamp$CraneUp & old.Stamp$SFCReset = new.Stamp$SFCReset & old.Stamp$StampLowered = new.Stamp$StampLowered & old.Stamp$StampSliderFilled = new.Stamp$StampSliderFilled & old.Stamp$StampSliderSensorMovedIn = new.Stamp$StampSliderSensorMovedIn & old.Stamp$StampSliderSensorMovedOut = new.Stamp$StampSliderSensorMovedOut & old.Stamp$StampStartButton = new.Stamp$StampStartButton & old.Stamp$StampUp = new.Stamp$StampUp & old.Stamp$StartVar = new.Stamp$StartVar[0m [[33mmodularization.kt:209[0m]
[     0.941] (INFO) [37m	Output-Relation: old.Stamp$StampGreenLamp = new.Stamp$StampGreenLamp & old.Stamp$StampPressure = new.Stamp$StampPressure & old.Stamp$StampPusher = new.Stamp$StampPusher & old.Stamp$StampSliderMovedIn = new.Stamp$StampSliderMovedIn & old.Stamp$StampSliderMovedOut = new.Stamp$StampSliderMovedOut & old.Stamp$StampWhiteLamp = new.Stamp$StampWhiteLamp & old.Stamp$StartCommandStamp = new.Stamp$StartCommandStamp[0m [[33mmodularization.kt:210[0m]
[     0.941] (INFO) [37mMatched Main.Crane.TimeDelay_Timer.0 to Main.Crane.TimeDelay_Timer.0[0m [[33mmodularization.kt:206[0m]
[     0.941] (INFO) [37m	Is perfect?: true[0m [[33mmodularization.kt:207[0m]
[     0.941] (INFO) [37m	Context: TRUE[0m [[33mmodularization.kt:208[0m]
[     0.941] (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:209[0m]
[     0.941] (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:210[0m]
[     0.941] (INFO) [37mOutput folder: output_1[0m [[33mapp.kt:118[0m]
[     0.942] (INFO) [37mStart with the proof[0m [[33mapp.kt:119[0m]
[     0.953] (INFO) [37mproofEquivalence(Main,Main):  Main.0: (LoC:759) (Vars: [75] (22) => (30))[0m [[33mstrategy.kt:71[0m]
[     0.961] (INFO) [37mproofEquivalence(Main,Main):  Main.0: (LoC:846) (Vars: [75] (22) => (32))[0m [[33mstrategy.kt:72[0m]
[     0.962] (INFO) [37mcheckCache(Main,Main):  Skipped because `disableCheckCache` is set[0m [[33mstrategy.kt:106[0m]
[     0.962] (INFO) [37mproofBodyEquivalenceSource(Main,Main):  Skipped because `disableProofBodyEquivalenceSource` is set[0m [[33mstrategy.kt:329[0m]
[     0.962] (INFO) [37mproofBodyEquivalenceSSA(Main,Main):  Skipped because `disableProofBodyEquivalenceSSA` is set[0m [[33mstrategy.kt:349[0m]
[     0.963] (INFO) [37mproofBodyEquivalenceSMT(Main,Main):  Skipped because `disableProofBodyEquivalenceSMT` is set[0m [[33mstrategy.kt:374[0m]
[     0.964] (INFO) [37mproofBodyEquivalenceWithAbstraction(Main,Main):  Skipped because `disableProofBodyEquivalenceWithAbstraction` is set[0m [[33mstrategy.kt:202[0m]
[     1.067] (INFO) [37mproofBodyEquivalenceClassic(Main,Main):  Starting proof: output_1/Main_Main.smv, output_1/Main_Main.log[0m [[33mstrategy.kt:163[0m]
[     1.119] (INFO) [37mrunNuXmv: Run solver on output_1/Main_Main.smv[0m [[33mstrategy.kt:486[0m]
[     1.120] (INFO) [37mCreate nuXmv command file `output_1/ic3.xmv'[0m [[33mstrategy.kt:505[0m]
[     1.121] (INFO) [37m/home/weigl/share/nuXmv-1.1.1-Linux/bin/nuXmv -int /home/weigl/work/verifaps-lib/aps-rvt/examples/ppumod/03_05/output_1/Main_Main.smv[0m [[33mstrategy.kt:819[0m]
[   748.829] (INFO) [37mrunNuXmv: Solver finished for output_1/Main_Main.smv with edu.kit.iti.formal.smv.NuXMVOutput$Verified@7d446ed1[0m [[33mstrategy.kt:490[0m]
[   748.831] (INFO) [37mproofBodyEquivalenceClassic(Main,Main):  Equality proven[0m [[33mstrategy.kt:168[0m]
[   748.831] (INFO) [37mupdateCache(Main,Main):  Skipped because `disableUpdateCache` is set[0m [[33mstrategy.kt:125[0m]
[   748.832] (INFO) [37mproofEquivalence(Main,Main):  Timings: {cache=0, cmc=747867, mod=1, smt=0, src=0, ssa=1}[0m [[33mstrategy.kt:96[0m]
[   748.832] (INFO) [37mProof result: true[0m [[33mmodularization.kt:219[0m]
