triplex_voter.lus.mcmt

(define-state-type state ((|%init| Bool) (|signal| Real) (|errorA| Real) (|errorB| Real) (|errorC| Real) (|output| Real) (|difference| Real) (|sensedA| Real) (|sensedB| Real) (|sensedC| Real) (|equalizedA| Real) (|equalizedB| Real) (|equalizedC| Real) (|equalizationA| Real) (|equalizationB| Real) (|equalizationC| Real) (|pre_output| Real) (|centering| Real) (|pre_equalizedA| Real) (|pre_equalizedB| Real) (|pre_equalizedC| Real) (|lemmaA| Bool) (|lemmaB| Bool) (|lemmaC| Bool) (|ok1| Bool) (|ok2| Bool) (|ok3| Bool) (|ok4| Bool) (|ok5| Bool) (|abs~0.a| Real) (|abs~0.out| Real) (|abs~1.a| Real) (|abs~1.out| Real) (|abs~2.a| Real) (|abs~2.out| Real) (|middleValue~0.a| Real) (|middleValue~0.b| Real) (|middleValue~0.c| Real) (|middleValue~0.out| Real) (|equalization~0.centering_value| Real) (|equalization~0.equalized_value| Real) (|equalization~0.output_value| Real) (|equalization~0.equalization_value| Real) (|equalization~0.sum1| Real) (|equalization~0.sum2| Real) (|equalization~0.sat1| Real) (|equalization~0.sat2| Real) (|equalization~1.centering_value| Real) (|equalization~1.equalized_value| Real) (|equalization~1.output_value| Real) (|equalization~1.equalization_value| Real) (|equalization~1.sum1| Real) (|equalization~1.sum2| Real) (|equalization~1.sat1| Real) (|equalization~1.sat2| Real) (|equalization~2.centering_value| Real) (|equalization~2.equalized_value| Real) (|equalization~2.output_value| Real) (|equalization~2.equalization_value| Real) (|equalization~2.sum1| Real) (|equalization~2.sum2| Real) (|equalization~2.sat1| Real) (|equalization~2.sat2| Real) (|middleValue~1.a| Real) (|middleValue~1.b| Real) (|middleValue~1.c| Real) (|middleValue~1.out| Real) (|abs~3.a| Real) (|abs~3.out| Real) (|abs~4.a| Real) (|abs~4.out| Real) (|abs~5.a| Real) (|abs~5.out| Real) (|abs~6.a| Real) (|abs~6.out| Real) (|abs~7.a| Real) (|abs~7.out| Real) (|abs~8.a| Real) (|abs~8.out| Real) (|abs~9.a| Real) (|abs~9.out| Real) (|abs~10.a| Real) (|abs~10.out| Real) (|abs~11.a| Real) (|abs~11.out| Real) (|equalization~0.saturation~0.lower_limit| Real) (|equalization~0.saturation~0.upper_limit| Real) (|equalization~0.saturation~0.signal| Real) (|equalization~0.saturation~0.out| Real) (|equalization~0.saturation~1.lower_limit| Real) (|equalization~0.saturation~1.upper_limit| Real) (|equalization~0.saturation~1.signal| Real) (|equalization~0.saturation~1.out| Real) (|equalization~1.saturation~0.lower_limit| Real) (|equalization~1.saturation~0.upper_limit| Real) (|equalization~1.saturation~0.signal| Real) (|equalization~1.saturation~0.out| Real) (|equalization~1.saturation~1.lower_limit| Real) (|equalization~1.saturation~1.upper_limit| Real) (|equalization~1.saturation~1.signal| Real) (|equalization~1.saturation~1.out| Real) (|equalization~2.saturation~0.lower_limit| Real) (|equalization~2.saturation~0.upper_limit| Real) (|equalization~2.saturation~0.signal| Real) (|equalization~2.saturation~0.out| Real) (|equalization~2.saturation~1.lower_limit| Real) (|equalization~2.saturation~1.upper_limit| Real) (|equalization~2.saturation~1.signal| Real) (|equalization~2.saturation~1.out| Real)))

(define-transition-system T state |%init| (and (and (= next.|abs~0.a| next.|errorA|) (= next.|abs~0.out| (ite (>= next.|abs~0.a| (/ 0 1)) next.|abs~0.a| (- next.|abs~0.a|))) (= next.|abs~1.a| next.|errorB|) (= next.|abs~1.out| (ite (>= next.|abs~1.a| (/ 0 1)) next.|abs~1.a| (- next.|abs~1.a|))) (= next.|abs~2.a| next.|errorC|) (= next.|abs~2.out| (ite (>= next.|abs~2.a| (/ 0 1)) next.|abs~2.a| (- next.|abs~2.a|))) (= next.|sensedA| (+ next.|signal| next.|errorA|)) (= next.|sensedB| (+ next.|signal| next.|errorB|)) (= next.|sensedC| (+ next.|signal| next.|errorC|)) (= next.|centering| (ite state.|%init| (/ 0 1) state.|middleValue~0.out|)) (= next.|pre_output| (ite state.|%init| (/ 0 1) state.|output|)) (= next.|pre_equalizedA| (ite state.|%init| (/ 0 1) state.|equalizedA|)) (= next.|pre_equalizedB| (ite state.|%init| (/ 0 1) state.|equalizedB|)) (= next.|pre_equalizedC| (ite state.|%init| (/ 0 1) state.|equalizedC|)) (= next.|equalizationA| next.|equalization~0.equalization_value|) (= next.|equalizationB| next.|equalization~1.equalization_value|) (= next.|equalizationC| next.|equalization~2.equalization_value|) (= next.|equalizedA| (- next.|sensedA| next.|equalizationA|)) (= next.|equalizedB| (- next.|sensedB| next.|equalizationB|)) (= next.|equalizedC| (- next.|sensedC| next.|equalizationC|)) (= next.|output| next.|middleValue~1.out|) (= next.|difference| (- next.|output| next.|signal|)) (= next.|lemmaA| (< next.|abs~3.out| (* (/ 2 1) (/ 3 20)))) (= next.|lemmaB| (< next.|abs~4.out| (* (/ 2 1) (/ 3 20)))) (= next.|lemmaC| (< next.|abs~5.out| (* (/ 2 1) (/ 3 20)))) (= next.|ok1| (< next.|abs~6.out| next.|abs~7.out|)) (= next.|ok2| (< next.|abs~6.out| next.|abs~8.out|)) (= next.|ok3| (< next.|abs~6.out| next.|abs~9.out|)) (= next.|ok4| (< next.|abs~6.out| next.|abs~10.out|)) (= next.|ok5| (< next.|abs~6.out| next.|abs~11.out|)) (= next.|middleValue~0.a| next.|equalizationA|) (= next.|middleValue~0.b| next.|equalizationB|) (= next.|middleValue~0.c| next.|equalizationC|) (= next.|middleValue~0.out| (ite (< next.|middleValue~0.a| next.|middleValue~0.b|) (ite (< next.|middleValue~0.b| next.|middleValue~0.c|) next.|middleValue~0.b| (ite (< next.|middleValue~0.c| next.|middleValue~0.a|) next.|middleValue~0.a| next.|middleValue~0.c|)) (ite (< next.|middleValue~0.a| next.|middleValue~0.c|) next.|middleValue~0.a| (ite (< next.|middleValue~0.c| next.|middleValue~0.b|) next.|middleValue~0.b| next.|middleValue~0.c|)))) (= next.|equalization~0.centering_value| next.|centering|) (= next.|equalization~0.equalized_value| next.|pre_equalizedA|) (= next.|equalization~0.output_value| next.|pre_output|) (= next.|equalization~0.sum1| (- next.|equalization~0.equalized_value| next.|equalization~0.output_value|)) (= next.|equalization~0.sat1| next.|equalization~0.saturation~0.out|) (= next.|equalization~0.sat2| next.|equalization~0.saturation~1.out|) (= next.|equalization~0.sum2| (- next.|equalization~0.sat1| next.|equalization~0.sat2|)) (= next.|equalization~0.equalization_value| (+ (* next.|equalization~0.sum2| (/ 1 5)) (ite state.|%init| (/ 0 1) state.|equalization~0.equalization_value|))) (= next.|equalization~1.centering_value| next.|centering|) (= next.|equalization~1.equalized_value| next.|pre_equalizedB|) (= next.|equalization~1.output_value| next.|pre_output|) (= next.|equalization~1.sum1| (- next.|equalization~1.equalized_value| next.|equalization~1.output_value|)) (= next.|equalization~1.sat1| next.|equalization~1.saturation~0.out|) (= next.|equalization~1.sat2| next.|equalization~1.saturation~1.out|) (= next.|equalization~1.sum2| (- next.|equalization~1.sat1| next.|equalization~1.sat2|)) (= next.|equalization~1.equalization_value| (+ (* next.|equalization~1.sum2| (/ 1 5)) (ite state.|%init| (/ 0 1) state.|equalization~1.equalization_value|))) (= next.|equalization~2.centering_value| next.|centering|) (= next.|equalization~2.equalized_value| next.|pre_equalizedC|) (= next.|equalization~2.output_value| next.|pre_output|) (= next.|equalization~2.sum1| (- next.|equalization~2.equalized_value| next.|equalization~2.output_value|)) (= next.|equalization~2.sat1| next.|equalization~2.saturation~0.out|) (= next.|equalization~2.sat2| next.|equalization~2.saturation~1.out|) (= next.|equalization~2.sum2| (- next.|equalization~2.sat1| next.|equalization~2.sat2|)) (= next.|equalization~2.equalization_value| (+ (* next.|equalization~2.sum2| (/ 1 5)) (ite state.|%init| (/ 0 1) state.|equalization~2.equalization_value|))) (= next.|middleValue~1.a| next.|equalizedA|) (= next.|middleValue~1.b| next.|equalizedB|) (= next.|middleValue~1.c| next.|equalizedC|) (= next.|middleValue~1.out| (ite (< next.|middleValue~1.a| next.|middleValue~1.b|) (ite (< next.|middleValue~1.b| next.|middleValue~1.c|) next.|middleValue~1.b| (ite (< next.|middleValue~1.c| next.|middleValue~1.a|) next.|middleValue~1.a| next.|middleValue~1.c|)) (ite (< next.|middleValue~1.a| next.|middleValue~1.c|) next.|middleValue~1.a| (ite (< next.|middleValue~1.c| next.|middleValue~1.b|) next.|middleValue~1.b| next.|middleValue~1.c|)))) (= next.|abs~3.a| (- next.|equalizedA| next.|sensedA|)) (= next.|abs~3.out| (ite (>= next.|abs~3.a| (/ 0 1)) next.|abs~3.a| (- next.|abs~3.a|))) (= next.|abs~4.a| (- next.|equalizedB| next.|sensedB|)) (= next.|abs~4.out| (ite (>= next.|abs~4.a| (/ 0 1)) next.|abs~4.a| (- next.|abs~4.a|))) (= next.|abs~5.a| (- next.|equalizedC| next.|sensedC|)) (= next.|abs~5.out| (ite (>= next.|abs~5.a| (/ 0 1)) next.|abs~5.a| (- next.|abs~5.a|))) (= next.|abs~6.a| next.|difference|) (= next.|abs~6.out| (ite (>= next.|abs~6.a| (/ 0 1)) next.|abs~6.a| (- next.|abs~6.a|))) (= next.|abs~7.a| (* (/ 3 20) (/ 3 1))) (= next.|abs~7.out| (ite (>= next.|abs~7.a| (/ 0 1)) next.|abs~7.a| (- next.|abs~7.a|))) (= next.|abs~8.a| (* (/ 3 20) (/ 13 5))) (= next.|abs~8.out| (ite (>= next.|abs~8.a| (/ 0 1)) next.|abs~8.a| (- next.|abs~8.a|))) (= next.|abs~9.a| (* (/ 3 20) (/ 49 20))) (= next.|abs~9.out| (ite (>= next.|abs~9.a| (/ 0 1)) next.|abs~9.a| (- next.|abs~9.a|))) (= next.|abs~10.a| (* (/ 3 20) (/ 47 20))) (= next.|abs~10.out| (ite (>= next.|abs~10.a| (/ 0 1)) next.|abs~10.a| (- next.|abs~10.a|))) (= next.|abs~11.a| (* (/ 3 20) (/ 23 10))) (= next.|abs~11.out| (ite (>= next.|abs~11.a| (/ 0 1)) next.|abs~11.a| (- next.|abs~11.a|))) (= next.|equalization~0.saturation~0.lower_limit| (- (/ 1 2))) (= next.|equalization~0.saturation~0.upper_limit| (/ 1 2)) (= next.|equalization~0.saturation~0.signal| next.|equalization~0.sum1|) (= next.|equalization~0.saturation~0.out| (ite (< next.|equalization~0.saturation~0.signal| next.|equalization~0.saturation~0.lower_limit|) next.|equalization~0.saturation~0.lower_limit| (ite (> next.|equalization~0.saturation~0.signal| next.|equalization~0.saturation~0.upper_limit|) next.|equalization~0.saturation~0.upper_limit| next.|equalization~0.saturation~0.signal|))) (= next.|equalization~0.saturation~1.lower_limit| (- (/ 1 4))) (= next.|equalization~0.saturation~1.upper_limit| (/ 1 4)) (= next.|equalization~0.saturation~1.signal| next.|equalization~0.centering_value|) (= next.|equalization~0.saturation~1.out| (ite (< next.|equalization~0.saturation~1.signal| next.|equalization~0.saturation~1.lower_limit|) next.|equalization~0.saturation~1.lower_limit| (ite (> next.|equalization~0.saturation~1.signal| next.|equalization~0.saturation~1.upper_limit|) next.|equalization~0.saturation~1.upper_limit| next.|equalization~0.saturation~1.signal|))) (= next.|equalization~1.saturation~0.lower_limit| (- (/ 1 2))) (= next.|equalization~1.saturation~0.upper_limit| (/ 1 2)) (= next.|equalization~1.saturation~0.signal| next.|equalization~1.sum1|) (= next.|equalization~1.saturation~0.out| (ite (< next.|equalization~1.saturation~0.signal| next.|equalization~1.saturation~0.lower_limit|) next.|equalization~1.saturation~0.lower_limit| (ite (> next.|equalization~1.saturation~0.signal| next.|equalization~1.saturation~0.upper_limit|) next.|equalization~1.saturation~0.upper_limit| next.|equalization~1.saturation~0.signal|))) (= next.|equalization~1.saturation~1.lower_limit| (- (/ 1 4))) (= next.|equalization~1.saturation~1.upper_limit| (/ 1 4)) (= next.|equalization~1.saturation~1.signal| next.|equalization~1.centering_value|) (= next.|equalization~1.saturation~1.out| (ite (< next.|equalization~1.saturation~1.signal| next.|equalization~1.saturation~1.lower_limit|) next.|equalization~1.saturation~1.lower_limit| (ite (> next.|equalization~1.saturation~1.signal| next.|equalization~1.saturation~1.upper_limit|) next.|equalization~1.saturation~1.upper_limit| next.|equalization~1.saturation~1.signal|))) (= next.|equalization~2.saturation~0.lower_limit| (- (/ 1 2))) (= next.|equalization~2.saturation~0.upper_limit| (/ 1 2)) (= next.|equalization~2.saturation~0.signal| next.|equalization~2.sum1|) (= next.|equalization~2.saturation~0.out| (ite (< next.|equalization~2.saturation~0.signal| next.|equalization~2.saturation~0.lower_limit|) next.|equalization~2.saturation~0.lower_limit| (ite (> next.|equalization~2.saturation~0.signal| next.|equalization~2.saturation~0.upper_limit|) next.|equalization~2.saturation~0.upper_limit| next.|equalization~2.saturation~0.signal|))) (= next.|equalization~2.saturation~1.lower_limit| (- (/ 1 4))) (= next.|equalization~2.saturation~1.upper_limit| (/ 1 4)) (= next.|equalization~2.saturation~1.signal| next.|equalization~2.centering_value|) (= next.|equalization~2.saturation~1.out| (ite (< next.|equalization~2.saturation~1.signal| next.|equalization~2.saturation~1.lower_limit|) next.|equalization~2.saturation~1.lower_limit| (ite (> next.|equalization~2.saturation~1.signal| next.|equalization~2.saturation~1.upper_limit|) next.|equalization~2.saturation~1.upper_limit| next.|equalization~2.saturation~1.signal|)))) (and (<= next.|abs~0.out| (/ 3 20)) (<= next.|abs~1.out| (/ 3 20)) (<= next.|abs~2.out| (/ 3 20))) true (not next.|%init|)))

(query T (or |lemmaA| |%init|))
(query T (or |lemmaB| |%init|))
(query T (or |lemmaC| |%init|))
(query T (or |ok1| |%init|))
(query T (or |ok2| |%init|))
(query T (or |ok3| |%init|))
(query T (or |ok4| |%init|))
(query T (or |ok5| |%init|))

I see that this has been translated from a lustre program. Do you have a translator?
I am not a fan of the encoding (having a "fake" initial state"), but if it's available it would be a very useful tool.