find_fault.sh (indexpetri0)

damasceno@princeton-lnx:~/git/fault-identification-in-petri-nets$ ./find_fault.sh 
[f_p1 >= 0,
 f_p2 >= 0,
 f_p3 >= 0,
 p1_f >= 0,
 p2_f >= 0,
 p3_f >= 0,
 l0 >= 0,
 Exists(l0,
        And(0 + l0*(f_p1 - p1_f) >= 0,
            0 + l0*(f_p2 - p2_f) >= 0,
            1 + l0*(f_p3 - p3_f) >= 1)),
 l1 >= 1,
 Exists(l1,
        And(0 + l1*(f_p1 - p1_f) >= 1,
            0 + l1*(f_p2 - p2_f) >= 0,
            1 + l1*(f_p3 - p3_f) >= 0)),
 l2 >= 1,
 Exists(l2,
        And(-1 + l2*(f_p1 - p1_f) >= 0,
            1 + l2*(f_p2 - p2_f) >= 1,
            1 + l2*(f_p3 - p3_f) >= 0)),
 l3 >= 1,
 Exists(l3,
        And(0 + l3*(f_p1 - p1_f) >= 1,
            0 + l3*(f_p2 - p2_f) >= 0,
            1 + l3*(f_p3 - p3_f) >= 0)),
 l4 >= 0,
 ForAll(l4,
        Or(0 + l4*(f_p1 - p1_f) < 0,
           0 + l4*(f_p2 - p2_f) < 1,
           1 + l4*(f_p3 - p3_f) < 0)),
 l5 >= 0,
 ForAll(l5,
        Or(-1 + l5*(f_p1 - p1_f) < 1,
           1 + l5*(f_p2 - p2_f) < 0,
           1 + l5*(f_p3 - p3_f) < 0)),
 l6 >= 0,
 ForAll(l6,
        Or(-1 + l6*(f_p1 - p1_f) < 0,
           1 + l6*(f_p2 - p2_f) < 0,
           1 + l6*(f_p3 - p3_f) < 1)),
 l7 >= 0,
 ForAll(l7,
        Or(0 + l7*(f_p1 - p1_f) < 1,
           0 + l7*(f_p2 - p2_f) < 0,
           0 + l7*(f_p3 - p3_f) < 0)),
 l8 >= 0,
 ForAll(l8,
        Or(0 + l8*(f_p1 - p1_f) < 0,
           0 + l8*(f_p2 - p2_f) < 1,
           0 + l8*(f_p3 - p3_f) < 0)),
 l9 >= 0,
 ForAll(l9,
        Or(0 + l9*(f_p1 - p1_f) < 0,
           0 + l9*(f_p2 - p2_f) < 0,
           0 + l9*(f_p3 - p3_f) < 1)),
 l10 >= 0,
 ForAll(l10,
        Or(0 + l10*(f_p1 - p1_f) < 0,
           0 + l10*(f_p2 - p2_f) < 1,
           1 + l10*(f_p3 - p3_f) < 0)),
 l11 >= 0,
 ForAll(l11,
        Or(0 + l11*(f_p1 - p1_f) < 0,
           0 + l11*(f_p2 - p2_f) < 0,
           1 + l11*(f_p3 - p3_f) < 1))]
unsat