example.java.out

findSchedulerModel

Z3 Major Version: 4
Z3 Full Version: 4.8.0.0
Z3 Full Version String: Z3 4.8.0.0

Rules set. Checking solver.
Current time of the day: 06:22:14.778
(define-fun flow1Fragment1ScheduledTime4 () Real
  (/ 15453081782.0 3081913.0))
(define-fun flow1Fragment1ScheduledTime5 () Real
  (/ 58687267346.0 9245739.0))
(define-fun flow1Fragment4ScheduledTime0 () Real
  (/ 3171906564.0 3081913.0))
(define-fun cycle57Duration () Real
  400.0)
(define-fun flow1Fragment4ScheduledTime1 () Real
  (/ 6253449564.0 3081913.0))
(define-fun flow1Fragment5ScheduledTime4 () Real
  (/ 15506218564.0 3081913.0))
(define-fun flow1Fragment6ScheduledTime1 () Real
  (/ 6250859564.0 3081913.0))
(define-fun cycle71Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun flow1Fragment5ScheduledTime5 () Real
  (/ 18581101564.0 3081913.0))
(define-fun flow1Fragment1ScheduledTime2 () Real
  (/ 89765648038.0 27737217.0))
(define-fun slotflow1Fragment1PriorityStart () Real
  (/ 11959668179.0 27737217.0))
(define-fun flow1Fragment4Priority () Int
  1)
(define-fun flow1Fragment4ScheduledTime2 () Real
  (/ 9334992564.0 3081913.0))
(define-fun cycle1Duration () Real
  400.0)
(define-fun flow1Fragment2ScheduledTime2 () Real
  (/ 89772308038.0 27737217.0))
(define-fun slotflow1Fragment5PriorityStart () Real
  (/ 2590000.0 3081913.0))
(define-fun flow1Fragment2ScheduledTime4 () Real
  (/ 15453821782.0 3081913.0))
(define-fun flow1Fragment4ScheduledTime4 () Real
  (/ 15498078564.0 3081913.0))
(define-fun cycle29Duration () Real
  400.0)
(define-fun flow1Fragment3ScheduledTime0 () Real
  (/ 3178042348.0 3081913.0))
(define-fun flow1Fragment4ScheduledTime5 () Real
  (/ 18579621564.0 3081913.0))
(define-fun flow1Fragment5ScheduledTime1 () Real
  (/ 6251599564.0 3081913.0))
(define-fun slotflow1Fragment3PriorityStart () Real
  (/ 2925782350.0 3081913.0))
(define-fun flow1Fragment1ScheduledTime1 () Real
  (/ 21704311346.0 9245739.0))
(define-fun flow1Fragment3ScheduledTime3 () Real
  (/ 730691817.0 181289.0))
(define-fun slotflow1Fragment2PriorityStart () Real
  (/ 11962998179.0 27737217.0))
(define-fun flow1Fragment6ScheduledTime3 () Real
  (/ 12529456345.0 3081913.0))
(define-fun slotflow1Fragment6PriorityDuration () Real
  50.0)
(define-fun flow1Fragment2ScheduledTime0 () Real
  (/ 3125799782.0 3081913.0))
(define-fun cycle113Duration () Real
  400.0)
(define-fun cycle127Start () Real
  (/ 204209345.0 3081913.0))
(define-fun slotflow1Fragment4PriorityStart () Real
  (/ 2926152350.0 3081913.0))
(define-fun flow1Fragment4ScheduledTime3 () Real
  (/ 12416535564.0 3081913.0))
(define-fun cycle43Duration () Real
  400.0)
(define-fun flow1Fragment2ScheduledTime3 () Real
  (/ 114425022038.0 27737217.0))
(define-fun flow1Fragment1ScheduledTime3 () Real
  (/ 114421692038.0 27737217.0))
(define-fun flow1Fragment3Priority () Int
  1)
(define-fun slotflow1Fragment2PriorityDuration () Real
  (/ 40434869.0 3081913.0))
(define-fun slotflow1Fragment4PriorityDuration () Real
  (/ 41544869.0 3081913.0))
(define-fun flow1Fragment2ScheduledTime1 () Real
  (/ 21705421346.0 9245739.0))
(define-fun cycle127Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun slotflow1Fragment6PriorityStart () Real
  (/ 1850000.0 3081913.0))
(define-fun flow1Fragment6ScheduledTime0 () Real
  (/ 3168946564.0 3081913.0))
(define-fun dev50FirstT1Time () Real
  1000.0)
(define-fun cycle99Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun flow1Fragment6ScheduledTime2 () Real
  (/ 9341507228.0 3081913.0))
(define-fun cycle99Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun flow1Fragment3ScheduledTime5 () Real
  6028.0)
(define-fun flow1Fragment6Priority () Int
  1)
(define-fun flow1Fragment3ScheduledTime1 () Real
  (/ 6257490852.0 3081913.0))
(define-fun cycle15Duration () Real
  400.0)
(define-fun flow1Fragment3ScheduledTime2 () Real
  (/ 9333947684.0 3081913.0))
(define-fun flow1Fragment5Priority () Int
  1)
(define-fun flow1Fragment1Priority () Int
  1)
(define-fun flow1Fragment3ScheduledTime4 () Real
  (/ 15505425876.0 3081913.0))
(define-fun flow1Fragment5ScheduledTime2 () Real
  (/ 9333882564.0 3081913.0))
(define-fun flow1Fragment5ScheduledTime3 () Real
  (/ 12419896866.0 3081913.0))
(define-fun cycle85Duration () Real
  400.0)
(define-fun slotflow1Fragment3PriorityDuration () Real
  50.0)
(define-fun flow1Fragment1ScheduledTime0 () Real
  1014.0)
(define-fun flow1Fragment2ScheduledTime5 () Real
  (/ 58689487346.0 9245739.0))
(define-fun flow1Fragment2Priority () Int
  1)
(define-fun flow1Fragment5ScheduledTime0 () Real
  (/ 186766764.0 181289.0))
(define-fun flow1Fragment6ScheduledTime5 () Real
  (/ 18580361564.0 3081913.0))
(define-fun slotflow1Fragment5PriorityDuration () Real
  50.0)
(define-fun slotflow1Fragment1PriorityDuration () Real
  (/ 40804869.0 3081913.0))
(define-fun cycle71Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun flow1Fragment6ScheduledTime4 () Real
  (/ 15506218564.0 3081913.0))
(define-fun cycle113Start () Real
  0.0)
(define-fun cycle85Start () Real
  0.0)
(define-fun cycle57Start () Real
  0.0)
(define-fun cycle43Start () Real
  0.0)
(define-fun cycle29Start () Real
  0.0)
(define-fun cycle15Start () Real
  0.0)
(define-fun cycle1Start () Real
  0.0)
(define-fun flow1JitterOfPacket0Fordev26 () Real
  (/ 9990000.0 3081913.0))
(define-fun flow1JitterOfPacket1Fordev26 () Real
  (/ 9990000.0 3081913.0))
(define-fun flow1JitterOfPacket2Fordev26 () Real
  (/ 1255336.0 3081913.0))
(define-fun flow1JitterOfPacket3Fordev26 () Real
  (/ 104780781.0 3081913.0))
(define-fun flow1JitterOfPacket4Fordev26 () Real
  (/ 370000.0 3081913.0))
(define-fun flow1JitterOfPacket0Fordev25 () Real
  (/ 3901576.0 3081913.0))
(define-fun flow1JitterOfPacket1Fordev25 () Real
  (/ 9250000.0 3081913.0))
(define-fun flow1JitterOfPacket2Fordev25 () Real
  (/ 8880000.0 3081913.0))
(define-fun flow1JitterOfPacket3Fordev25 () Real
  (/ 4778698.0 3081913.0))
(define-fun flow1JitterOfPacket4Fordev25 () Real
  (/ 370000.0 3081913.0))
(define-fun flow1JitterOfPacket0Fordev46 () Real
  (/ 7030000.0 3081913.0))
(define-fun flow1JitterOfPacket1Fordev46 () Real
  (/ 7400000.0 3081913.0))
(define-fun flow1JitterOfPacket2Fordev46 () Real
  (/ 7770000.0 3081913.0))
(define-fun flow1JitterOfPacket3Fordev46 () Real
  (/ 8140000.0 3081913.0))
(define-fun flow1JitterOfPacket4Fordev46 () Real
  (/ 8510000.0 3081913.0))
(define-fun flow1JitterOfPacket0Fordev45 () Real
  (/ 894216.0 3081913.0))
(define-fun flow1JitterOfPacket1Fordev45 () Real
  (/ 3358712.0 3081913.0))
(define-fun flow1JitterOfPacket2Fordev45 () Real
  (/ 8814880.0 3081913.0))
(define-fun flow1JitterOfPacket3Fordev45 () Real
  (/ 2914675.0 3081913.0))
(define-fun flow1JitterOfPacket4Fordev45 () Real
  (/ 1162688.0 3081913.0))
(define-fun flow1latencyOfPacket0Fordev26 () Real
  (/ 87033564.0 3081913.0))
(define-fun flow1latencyOfPacket1Fordev26 () Real
  (/ 87033564.0 3081913.0))
(define-fun flow1latencyOfPacket2Fordev26 () Real
  (/ 95768228.0 3081913.0))
(define-fun flow1latencyOfPacket3Fordev26 () Real
  (/ 201804345.0 3081913.0))
(define-fun flow1latencyOfPacket4Fordev26 () Real
  (/ 96653564.0 3081913.0))
(define-fun flow1latencyOfPacket0Fordev25 () Real
  (/ 5477764.0 181289.0))
(define-fun flow1latencyOfPacket1Fordev25 () Real
  (/ 87773564.0 3081913.0))
(define-fun flow1latencyOfPacket2Fordev25 () Real
  (/ 88143564.0 3081913.0))
(define-fun flow1latencyOfPacket3Fordev25 () Real
  (/ 92244866.0 3081913.0))
(define-fun flow1latencyOfPacket4Fordev25 () Real
  (/ 96653564.0 3081913.0))
(define-fun flow1latencyOfPacket0Fordev46 () Real
  (/ 89993564.0 3081913.0))
(define-fun flow1latencyOfPacket1Fordev46 () Real
  (/ 89623564.0 3081913.0))
(define-fun flow1latencyOfPacket2Fordev46 () Real
  (/ 89253564.0 3081913.0))
(define-fun flow1latencyOfPacket3Fordev46 () Real
  (/ 88883564.0 3081913.0))
(define-fun flow1latencyOfPacket4Fordev46 () Real
  (/ 88513564.0 3081913.0))
(define-fun flow1latencyOfPacket0Fordev45 () Real
  (/ 96129348.0 3081913.0))
(define-fun flow1latencyOfPacket1Fordev45 () Real
  (/ 93664852.0 3081913.0))
(define-fun flow1latencyOfPacket2Fordev45 () Real
  (/ 88208684.0 3081913.0))
(define-fun flow1latencyOfPacket3Fordev45 () Real
  (/ 5535817.0 181289.0))
(define-fun flow1latencyOfPacket4Fordev45 () Real
  (/ 95860876.0 3081913.0))
(define-fun cycle140Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle140Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle139Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle139Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle138Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle138Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle137Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle137Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle136Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle136Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle135Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle135Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle134Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle134Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle133Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle133Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle132Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle132Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle131Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle131Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle130Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle130Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle129Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle129Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle128Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycle128Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycleOfswitch9Start () Real
  (/ 204209345.0 3081913.0))
(define-fun cycleOfswitch9Duration () Real
  (/ 3081543000.0 3081913.0))
(define-fun cycle126Start () Real
  0.0)
(define-fun cycle126Duration () Real
  400.0)
(define-fun cycle125Start () Real
  0.0)
(define-fun cycle125Duration () Real
  400.0)
(define-fun cycle124Start () Real
  0.0)
(define-fun cycle124Duration () Real
  400.0)
(define-fun cycle123Start () Real
  0.0)
(define-fun cycle123Duration () Real
  400.0)
(define-fun cycle122Start () Real
  0.0)
(define-fun cycle122Duration () Real
  400.0)
(define-fun cycle121Start () Real
  0.0)
(define-fun cycle121Duration () Real
  400.0)
(define-fun cycle120Start () Real
  0.0)
(define-fun cycle120Duration () Real
  400.0)
(define-fun cycle119Start () Real
  0.0)
(define-fun cycle119Duration () Real
  400.0)
(define-fun cycle118Start () Real
  0.0)
(define-fun cycle118Duration () Real
  400.0)
(define-fun cycle117Start () Real
  0.0)
(define-fun cycle117Duration () Real
  400.0)
(define-fun cycle116Start () Real
  0.0)
(define-fun cycle116Duration () Real
  400.0)
(define-fun cycle115Start () Real
  0.0)
(define-fun cycle115Duration () Real
  400.0)
(define-fun cycle114Start () Real
  0.0)
(define-fun cycle114Duration () Real
  400.0)
(define-fun cycleOfswitch8Start () Real
  0.0)
(define-fun cycleOfswitch8Duration () Real
  400.0)
(define-fun cycle112Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle112Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle111Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle111Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle110Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle110Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle109Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle109Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle108Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle108Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle107Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle107Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle106Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle106Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle105Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle105Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle104Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle104Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle103Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle103Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle102Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle102Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle101Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle101Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle100Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycle100Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycleOfswitch7Start () Real
  (/ 3477264038.0 27737217.0))
(define-fun cycleOfswitch7Duration () Real
  (/ 12328022000.0 27737217.0))
(define-fun cycle98Start () Real
  0.0)
(define-fun cycle98Duration () Real
  400.0)
(define-fun cycle97Start () Real
  0.0)
(define-fun cycle97Duration () Real
  400.0)
(define-fun cycle96Start () Real
  0.0)
(define-fun cycle96Duration () Real
  400.0)
(define-fun cycle95Start () Real
  0.0)
(define-fun cycle95Duration () Real
  400.0)
(define-fun cycle94Start () Real
  0.0)
(define-fun cycle94Duration () Real
  400.0)
(define-fun cycle93Start () Real
  0.0)
(define-fun cycle93Duration () Real
  400.0)
(define-fun cycle92Start () Real
  0.0)
(define-fun cycle92Duration () Real
  400.0)
(define-fun cycle91Start () Real
  0.0)
(define-fun cycle91Duration () Real
  400.0)
(define-fun cycle90Start () Real
  0.0)
(define-fun cycle90Duration () Real
  400.0)
(define-fun cycle89Start () Real
  0.0)
(define-fun cycle89Duration () Real
  400.0)
(define-fun cycle88Start () Real
  0.0)
(define-fun cycle88Duration () Real
  400.0)
(define-fun cycle87Start () Real
  0.0)
(define-fun cycle87Duration () Real
  400.0)
(define-fun cycle86Start () Real
  0.0)
(define-fun cycle86Duration () Real
  400.0)
(define-fun cycleOfswitch6Start () Real
  0.0)
(define-fun cycleOfswitch6Duration () Real
  400.0)
(define-fun cycle84Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle84Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle83Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle83Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle82Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle82Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle81Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle81Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle80Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle80Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle79Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle79Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle78Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle78Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle77Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle77Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle76Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle76Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle75Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle75Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle74Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle74Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle73Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle73Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle72Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycle72Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycleOfswitch5Start () Real
  (/ 3126661695.0 3081913.0))
(define-fun cycleOfswitch5Duration () Real
  (/ 3082283000.0 3081913.0))
(define-fun cycle70Start () Real
  0.0)
(define-fun cycle70Duration () Real
  400.0)
(define-fun cycle69Start () Real
  0.0)
(define-fun cycle69Duration () Real
  400.0)
(define-fun cycle68Start () Real
  0.0)
(define-fun cycle68Duration () Real
  400.0)
(define-fun cycle67Start () Real
  0.0)
(define-fun cycle67Duration () Real
  400.0)
(define-fun cycle66Start () Real
  0.0)
(define-fun cycle66Duration () Real
  400.0)
(define-fun cycle65Start () Real
  0.0)
(define-fun cycle65Duration () Real
  400.0)
(define-fun cycle64Start () Real
  0.0)
(define-fun cycle64Duration () Real
  400.0)
(define-fun cycle63Start () Real
  0.0)
(define-fun cycle63Duration () Real
  400.0)
(define-fun cycle62Start () Real
  0.0)
(define-fun cycle62Duration () Real
  400.0)
(define-fun cycle61Start () Real
  0.0)
(define-fun cycle61Duration () Real
  400.0)
(define-fun cycle60Start () Real
  0.0)
(define-fun cycle60Duration () Real
  400.0)
(define-fun cycle59Start () Real
  0.0)
(define-fun cycle59Duration () Real
  400.0)
(define-fun cycle58Start () Real
  0.0)
(define-fun cycle58Duration () Real
  400.0)
(define-fun cycleOfswitch4Start () Real
  0.0)
(define-fun cycleOfswitch4Duration () Real
  400.0)
(define-fun cycle56Start () Real
  0.0)
(define-fun cycle56Duration () Real
  400.0)
(define-fun cycle55Start () Real
  0.0)
(define-fun cycle55Duration () Real
  400.0)
(define-fun cycle54Start () Real
  0.0)
(define-fun cycle54Duration () Real
  400.0)
(define-fun cycle53Start () Real
  0.0)
(define-fun cycle53Duration () Real
  400.0)
(define-fun cycle52Start () Real
  0.0)
(define-fun cycle52Duration () Real
  400.0)
(define-fun cycle51Start () Real
  0.0)
(define-fun cycle51Duration () Real
  400.0)
(define-fun cycle50Start () Real
  0.0)
(define-fun cycle50Duration () Real
  400.0)
(define-fun cycle49Start () Real
  0.0)
(define-fun cycle49Duration () Real
  400.0)
(define-fun cycle48Start () Real
  0.0)
(define-fun cycle48Duration () Real
  400.0)
(define-fun cycle47Start () Real
  0.0)
(define-fun cycle47Duration () Real
  400.0)
(define-fun cycle46Start () Real
  0.0)
(define-fun cycle46Duration () Real
  400.0)
(define-fun cycle45Start () Real
  0.0)
(define-fun cycle45Duration () Real
  400.0)
(define-fun cycle44Start () Real
  0.0)
(define-fun cycle44Duration () Real
  400.0)
(define-fun cycleOfswitch3Start () Real
  0.0)
(define-fun cycleOfswitch3Duration () Real
  400.0)
(define-fun cycle42Start () Real
  0.0)
(define-fun cycle42Duration () Real
  400.0)
(define-fun cycle41Start () Real
  0.0)
(define-fun cycle41Duration () Real
  400.0)
(define-fun cycle40Start () Real
  0.0)
(define-fun cycle40Duration () Real
  400.0)
(define-fun cycle39Start () Real
  0.0)
(define-fun cycle39Duration () Real
  400.0)
(define-fun cycle38Start () Real
  0.0)
(define-fun cycle38Duration () Real
  400.0)
(define-fun cycle37Start () Real
  0.0)
(define-fun cycle37Duration () Real
  400.0)
(define-fun cycle36Start () Real
  0.0)
(define-fun cycle36Duration () Real
  400.0)
(define-fun cycle35Start () Real
  0.0)
(define-fun cycle35Duration () Real
  400.0)
(define-fun cycle34Start () Real
  0.0)
(define-fun cycle34Duration () Real
  400.0)
(define-fun cycle33Start () Real
  0.0)
(define-fun cycle33Duration () Real
  400.0)
(define-fun cycle32Start () Real
  0.0)
(define-fun cycle32Duration () Real
  400.0)
(define-fun cycle31Start () Real
  0.0)
(define-fun cycle31Duration () Real
  400.0)
(define-fun cycle30Start () Real
  0.0)
(define-fun cycle30Duration () Real
  400.0)
(define-fun cycleOfswitch2Start () Real
  0.0)
(define-fun cycleOfswitch2Duration () Real
  400.0)
(define-fun cycle28Start () Real
  0.0)
(define-fun cycle28Duration () Real
  400.0)
(define-fun cycle27Start () Real
  0.0)
(define-fun cycle27Duration () Real
  400.0)
(define-fun cycle26Start () Real
  0.0)
(define-fun cycle26Duration () Real
  400.0)
(define-fun cycle25Start () Real
  0.0)
(define-fun cycle25Duration () Real
  400.0)
(define-fun cycle24Start () Real
  0.0)
(define-fun cycle24Duration () Real
  400.0)
(define-fun cycle23Start () Real
  0.0)
(define-fun cycle23Duration () Real
  400.0)
(define-fun cycle22Start () Real
  0.0)
(define-fun cycle22Duration () Real
  400.0)
(define-fun cycle21Start () Real
  0.0)
(define-fun cycle21Duration () Real
  400.0)
(define-fun cycle20Start () Real
  0.0)
(define-fun cycle20Duration () Real
  400.0)
(define-fun cycle19Start () Real
  0.0)
(define-fun cycle19Duration () Real
  400.0)
(define-fun cycle18Start () Real
  0.0)
(define-fun cycle18Duration () Real
  400.0)
(define-fun cycle17Start () Real
  0.0)
(define-fun cycle17Duration () Real
  400.0)
(define-fun cycle16Start () Real
  0.0)
(define-fun cycle16Duration () Real
  400.0)
(define-fun cycleOfswitch1Start () Real
  0.0)
(define-fun cycleOfswitch1Duration () Real
  400.0)
(define-fun cycle14Start () Real
  0.0)
(define-fun cycle14Duration () Real
  400.0)
(define-fun cycle13Start () Real
  0.0)
(define-fun cycle13Duration () Real
  400.0)
(define-fun cycle12Start () Real
  0.0)
(define-fun cycle12Duration () Real
  400.0)
(define-fun cycle11Start () Real
  0.0)
(define-fun cycle11Duration () Real
  400.0)
(define-fun cycle10Start () Real
  0.0)
(define-fun cycle10Duration () Real
  400.0)
(define-fun cycle9Start () Real
  0.0)
(define-fun cycle9Duration () Real
  400.0)
(define-fun cycle8Start () Real
  0.0)
(define-fun cycle8Duration () Real
  400.0)
(define-fun cycle7Start () Real
  0.0)
(define-fun cycle7Duration () Real
  400.0)
(define-fun cycle6Start () Real
  0.0)
(define-fun cycle6Duration () Real
  400.0)
(define-fun cycle5Start () Real
  0.0)
(define-fun cycle5Duration () Real
  400.0)
(define-fun cycle4Start () Real
  0.0)
(define-fun cycle4Duration () Real
  400.0)
(define-fun cycle3Start () Real
  0.0)
(define-fun cycle3Duration () Real
  400.0)
(define-fun cycle2Start () Real
  0.0)
(define-fun cycle2Duration () Real
  400.0)
(define-fun cycleOfswitch0Start () Real
  0.0)
(define-fun cycleOfswitch0Duration () Real
  400.0)
Model generated.


Execution time: 10.398512 seconds
 
Flow 0 average latency: 30.583332
Flow 0 average jitter: 3.041666

Number of nodes in the network: 3 
Number of flows in the network: 1 
Number of subscribers in the network: 4 
Overall average latency: 30.583332
Overall average jitter: 3.041666


PATH TREE:
    Path to dev45: dev37, switch7(flow1Fragment1), switch9(flow1Fragment3), dev45, 
    Path to dev46: dev37, switch7(flow1Fragment1), switch9(flow1Fragment4), dev46, 
    Path to dev25: dev37, switch7(flow1Fragment2), switch5(flow1Fragment5), dev25, 
    Path to dev26: dev37, switch7(flow1Fragment2), switch5(flow1Fragment6), dev26,