source: vis_dev/vis-2.1/examples/fpmpy/check_result @ 15

Last change on this file since 15 was 11, checked in by cecile, 13 years ago

Add vis
File size: 2.6 KB
Line 
1# INV: formula passed --- (((!((FPM.state<1>=0 * FPM.state<0>=0)) * ((((x<6>=0 * x<5>=0) * x<4>=0) * x<3>=0) -> ((x<2>=0 * x<1>=0) * x<0>=0))) * ((((y<6>=0 * y<5>=0) * y<4>=0) * y<3>=0) -> ((y<2>=0 * y<1>=0) * y<0>=0))) -> ((((z<6>=0 * z<5>=0) * z<4>=0) * z<3>=0) -> ((z<2>=0 * z<1>=0) * z<0>=0)))
2# INV: formula failed --- ((!((FPM.state<1>=0 * FPM.state<0>=0)) * !((y<7>=1 ^ x<7>=0))) -> z<7>=1)
3# MC: formula passed --- AG(((((start=1 * (FPM.state<1>=0 * FPM.state<0>=0)) * ((((y<6>=0 * y<5>=0) * y<4>=0) * y<3>=0) -> ((y<2>=0 * y<1>=0) * y<0>=0))) * ((((x<6>=0 * x<5>=0) * x<4>=0) * x<3>=0) -> ((x<2>=0 * x<1>=0) * x<0>=0))) -> AX(AX(AX(((((z<6>=0 * z<5>=0) * z<4>=0) * z<3>=0) -> ((z<2>=0 * z<1>=0) * z<0>=0)))))))
4# MC: formula failed --- AG((((start=1 * (FPM.state<1>=0 * FPM.state<0>=0)) * !((y<7>=1 ^ x<7>=0))) -> AX(AX(AX(z<7>=1)))))
5# MC: formula passed --- AG((((start=1 * (FPM.state<1>=0 * FPM.state<0>=0)) * (y<7>=1 ^ x<7>=0)) -> AX(AX(AX(z<7>=0)))))
6# MC: formula passed --- AG((((start=1 * (FPM.state<1>=0 * FPM.state<0>=0)) * (((((y<6>=1 * y<5>=1) * y<4>=1) * y<3>=1) * !(((y<2>=0 * y<1>=0) * y<0>=0))) + ((((x<6>=1 * x<5>=1) * x<4>=1) * x<3>=1) * !(((x<2>=0 * x<1>=0) * x<0>=0))))) -> AX(AX(AX(((((z<6>=1 * z<5>=1) * z<4>=1) * z<3>=1) * !(((z<2>=0 * z<1>=0) * z<0>=0))))))))
7# MC: formula failed --- AG(((((start=1 * (FPM.state<1>=0 * FPM.state<0>=0)) * ((((((y<6>=0 * y<5>=0) * y<4>=0) * y<3>=0) * y<2>=0) * y<1>=0) * y<0>=0)) * !(((((x<6>=1 * x<5>=1) * x<4>=1) * x<3>=1) * !(((x<2>=0 * x<1>=0) * x<0>=0))))) -> AX(AX(AX(((((((z<6>=0 * z<5>=0) * z<4>=0) * z<3>=0) * z<2>=0) * z<1>=0) * z<0>=0))))))
8# MC: formula failed --- AG(((((start=1 * (FPM.state<1>=0 * FPM.state<0>=0)) * ((((((x<6>=0 * x<5>=0) * x<4>=0) * x<3>=0) * x<2>=0) * x<1>=0) * x<0>=0)) * !(((((y<6>=1 * y<5>=1) * y<4>=1) * y<3>=1) * !(((y<2>=0 * y<1>=0) * y<0>=0))))) -> AX(AX(AX(((((((z<6>=0 * z<5>=0) * z<4>=0) * z<3>=0) * z<2>=0) * z<1>=0) * z<0>=0))))))
9# MC: formula passed --- AG((((((start=1 * (FPM.state<1>=0 * FPM.state<0>=0)) * ((((((y<6>=1 * y<5>=1) * y<4>=1) * y<3>=1) * y<2>=0) * y<1>=0) * y<0>=0)) * !(((((x<6>=1 * x<5>=1) * x<4>=1) * x<3>=1) * !(((x<2>=0 * x<1>=0) * x<0>=0))))) * !((((x<6>=0 * x<5>=0) * x<4>=0) * x<3>=0))) -> AX(AX(AX(((((((z<6>=1 * z<5>=1) * z<4>=1) * z<3>=1) * z<2>=0) * z<1>=0) * z<0>=0))))))
10# MC: formula passed --- AG((((((start=1 * (FPM.state<1>=0 * FPM.state<0>=0)) * ((((((x<6>=1 * x<5>=1) * x<4>=1) * x<3>=1) * x<2>=0) * x<1>=0) * x<0>=0)) * !(((((y<6>=1 * y<5>=1) * y<4>=1) * y<3>=1) * !(((y<2>=0 * y<1>=0) * y<0>=0))))) * !((((y<6>=0 * y<5>=0) * y<4>=0) * y<3>=0))) -> AX(AX(AX(((((((z<6>=1 * z<5>=1) * z<4>=1) * z<3>=1) * z<2>=0) * z<1>=0) * z<0>=0))))))
Note: See TracBrowser for help on using the repository browser.