Commit 89d2a43e authored by Joshua Moerman's avatar Joshua Moerman
Browse files

Adds extra invariant to disable invalid transitions

parent 44768447
......@@ -144,6 +144,52 @@ ASSIGN
esac;
INVAR !(input = null & output = null)
& !(input != null & output != null)
& !(state = s0 & input = iA)
& !(state = s0 & input = iC)
& !(state = s0 & input = iE)
& !(state = s1 & input = iB)
& !(state = s1 & input = iC)
& !(state = s1 & input = iD)
& !(state = s1 & input = iE)
& !(state = s10 & input = iA)
& !(state = s10 & input = iB)
& !(state = s10 & input = iC)
& !(state = s10 & input = iE)
& !(state = s11 & input = iA)
& !(state = s11 & input = iB)
& !(state = s11 & input = iE)
& !(state = s12 & input = iA)
& !(state = s12 & input = iB)
& !(state = s12 & input = iC)
& !(state = s12 & input = iD)
& !(state = s2 & input = iA)
& !(state = s2 & input = iB)
& !(state = s2 & input = iD)
& !(state = s2 & input = iE)
& !(state = s3 & input = iA)
& !(state = s3 & input = iB)
& !(state = s3 & input = iD)
& !(state = s3 & input = iE)
& !(state = s4 & input = iA)
& !(state = s4 & input = iB)
& !(state = s4 & input = iD)
& !(state = s4 & input = iE)
& !(state = s5 & input = iA)
& !(state = s5 & input = iB)
& !(state = s5 & input = iE)
& !(state = s6 & input = iA)
& !(state = s6 & input = iB)
& !(state = s7 & input = iA)
& !(state = s7 & input = iB)
& !(state = s7 & input = iC)
& !(state = s7 & input = iE)
& !(state = s8 & input = iB)
& !(state = s8 & input = iC)
& !(state = s8 & input = iE)
& !(state = s9 & input = iB)
& !(state = s9 & input = iC)
& !(state = s9 & input = iD)
& !(state = s9 & input = iE)
LTLSPEC (FALSE V (! (input = iC) | (TRUE U (((output = oU) & ! (output = oW)) & X (! (output = oW) U (output = oV))))))
LTLSPEC (FALSE V (! (input = iD) | ((! (((output = oS) & ! (input = iC)) & X (! (input = iC) U ((output = oY) & ! (input = iC)))) U ((input = iC) | (output = oU))) | (FALSE V ! ((output = oS) & X (TRUE U (output = oY)))))))
LTLSPEC (FALSE V (! ((output = oS) & (TRUE U (input = iB))) | (! (output = oV) U ((input = iB) | (((output = oW) & ! (output = oV)) & X (! (output = oV) U (output = oX)))))))
......
......@@ -144,3 +144,49 @@ ASSIGN
esac;
INVAR !(input = null & output = null)
& !(input != null & output != null)
& !(state = s0 & input = iA)
& !(state = s0 & input = iC)
& !(state = s0 & input = iE)
& !(state = s1 & input = iB)
& !(state = s1 & input = iC)
& !(state = s1 & input = iD)
& !(state = s1 & input = iE)
& !(state = s10 & input = iA)
& !(state = s10 & input = iB)
& !(state = s10 & input = iC)
& !(state = s10 & input = iE)
& !(state = s11 & input = iA)
& !(state = s11 & input = iB)
& !(state = s11 & input = iE)
& !(state = s12 & input = iA)
& !(state = s12 & input = iB)
& !(state = s12 & input = iC)
& !(state = s12 & input = iD)
& !(state = s2 & input = iA)
& !(state = s2 & input = iB)
& !(state = s2 & input = iD)
& !(state = s2 & input = iE)
& !(state = s3 & input = iA)
& !(state = s3 & input = iB)
& !(state = s3 & input = iD)
& !(state = s3 & input = iE)
& !(state = s4 & input = iA)
& !(state = s4 & input = iB)
& !(state = s4 & input = iD)
& !(state = s4 & input = iE)
& !(state = s5 & input = iA)
& !(state = s5 & input = iB)
& !(state = s5 & input = iE)
& !(state = s6 & input = iA)
& !(state = s6 & input = iB)
& !(state = s7 & input = iA)
& !(state = s7 & input = iB)
& !(state = s7 & input = iC)
& !(state = s7 & input = iE)
& !(state = s8 & input = iB)
& !(state = s8 & input = iC)
& !(state = s8 & input = iE)
& !(state = s9 & input = iB)
& !(state = s9 & input = iC)
& !(state = s9 & input = iD)
& !(state = s9 & input = iE)
......@@ -234,6 +234,72 @@ ASSIGN
esac;
INVAR !(input = null & output = null)
& !(input != null & output != null)
& !(state = s0 & input = iA)
& !(state = s0 & input = iB)
& !(state = s0 & input = iC)
& !(state = s0 & input = iE)
& !(state = s1 & input = iA)
& !(state = s1 & input = iB)
& !(state = s1 & input = iC)
& !(state = s10 & input = iA)
& !(state = s10 & input = iC)
& !(state = s11 & input = iC)
& !(state = s11 & input = iD)
& !(state = s12 & input = iA)
& !(state = s12 & input = iB)
& !(state = s12 & input = iC)
& !(state = s12 & input = iD)
& !(state = s13 & input = iA)
& !(state = s13 & input = iC)
& !(state = s13 & input = iD)
& !(state = s13 & input = iE)
& !(state = s14 & input = iA)
& !(state = s14 & input = iC)
& !(state = s14 & input = iD)
& !(state = s15 & input = iA)
& !(state = s15 & input = iB)
& !(state = s15 & input = iC)
& !(state = s15 & input = iD)
& !(state = s16 & input = iB)
& !(state = s16 & input = iC)
& !(state = s16 & input = iD)
& !(state = s17 & input = iC)
& !(state = s17 & input = iE)
& !(state = s18 & input = iB)
& !(state = s18 & input = iC)
& !(state = s19 & input = iC)
& !(state = s19 & input = iD)
& !(state = s2 & input = iB)
& !(state = s2 & input = iC)
& !(state = s2 & input = iD)
& !(state = s20 & input = iA)
& !(state = s20 & input = iC)
& !(state = s21 & input = iB)
& !(state = s21 & input = iC)
& !(state = s21 & input = iE)
& !(state = s3 & input = iA)
& !(state = s3 & input = iB)
& !(state = s3 & input = iC)
& !(state = s3 & input = iE)
& !(state = s4 & input = iA)
& !(state = s4 & input = iB)
& !(state = s4 & input = iC)
& !(state = s4 & input = iD)
& !(state = s5 & input = iC)
& !(state = s5 & input = iE)
& !(state = s6 & input = iA)
& !(state = s6 & input = iB)
& !(state = s6 & input = iC)
& !(state = s6 & input = iE)
& !(state = s7 & input = iB)
& !(state = s7 & input = iC)
& !(state = s7 & input = iE)
& !(state = s8 & input = iC)
& !(state = s8 & input = iD)
& !(state = s8 & input = iE)
& !(state = s9 & input = iC)
& !(state = s9 & input = iD)
& !(state = s9 & input = iE)
LTLSPEC (FALSE V ((output = oT) & (! ! (output = oY) | ((output = oY) V ((! (input = iA) | (! (output = oY) U ((output = oX) & ! (output = oY)))) | (output = oY))))))
LTLSPEC ((FALSE V ! (output = oS)) | (! (output = oS) U ((output = oS) & (! (TRUE U ((output = oW) & X (TRUE U (output = oY)))) | (! (output = oW) U (input = iE))))))
LTLSPEC (FALSE V (! (input = iC) | (FALSE V (! (input = iD) | ((output = oX) & X (TRUE U (output = oZ)))))))
......
......@@ -234,3 +234,69 @@ ASSIGN
esac;
INVAR !(input = null & output = null)
& !(input != null & output != null)
& !(state = s0 & input = iA)
& !(state = s0 & input = iB)
& !(state = s0 & input = iC)
& !(state = s0 & input = iE)
& !(state = s1 & input = iA)
& !(state = s1 & input = iB)
& !(state = s1 & input = iC)
& !(state = s10 & input = iA)
& !(state = s10 & input = iC)
& !(state = s11 & input = iC)
& !(state = s11 & input = iD)
& !(state = s12 & input = iA)
& !(state = s12 & input = iB)
& !(state = s12 & input = iC)
& !(state = s12 & input = iD)
& !(state = s13 & input = iA)
& !(state = s13 & input = iC)
& !(state = s13 & input = iD)
& !(state = s13 & input = iE)
& !(state = s14 & input = iA)
& !(state = s14 & input = iC)
& !(state = s14 & input = iD)
& !(state = s15 & input = iA)
& !(state = s15 & input = iB)
& !(state = s15 & input = iC)
& !(state = s15 & input = iD)
& !(state = s16 & input = iB)
& !(state = s16 & input = iC)
& !(state = s16 & input = iD)
& !(state = s17 & input = iC)
& !(state = s17 & input = iE)
& !(state = s18 & input = iB)
& !(state = s18 & input = iC)
& !(state = s19 & input = iC)
& !(state = s19 & input = iD)
& !(state = s2 & input = iB)
& !(state = s2 & input = iC)
& !(state = s2 & input = iD)
& !(state = s20 & input = iA)
& !(state = s20 & input = iC)
& !(state = s21 & input = iB)
& !(state = s21 & input = iC)
& !(state = s21 & input = iE)
& !(state = s3 & input = iA)
& !(state = s3 & input = iB)
& !(state = s3 & input = iC)
& !(state = s3 & input = iE)
& !(state = s4 & input = iA)
& !(state = s4 & input = iB)
& !(state = s4 & input = iC)
& !(state = s4 & input = iD)
& !(state = s5 & input = iC)
& !(state = s5 & input = iE)
& !(state = s6 & input = iA)
& !(state = s6 & input = iB)
& !(state = s6 & input = iC)
& !(state = s6 & input = iE)
& !(state = s7 & input = iB)
& !(state = s7 & input = iC)
& !(state = s7 & input = iE)
& !(state = s8 & input = iC)
& !(state = s8 & input = iD)
& !(state = s8 & input = iE)
& !(state = s9 & input = iC)
& !(state = s9 & input = iD)
& !(state = s9 & input = iE)
......@@ -534,6 +534,227 @@ ASSIGN
esac;
INVAR !(input = null & output = null)
& !(input != null & output != null)
& !(state = s0 & input = iB)
& !(state = s0 & input = iC)
& !(state = s0 & input = iD)
& !(state = s0 & input = iF)
& !(state = s0 & input = iG)
& !(state = s0 & input = iH)
& !(state = s0 & input = iI)
& !(state = s0 & input = iJ)
& !(state = s1 & input = iB)
& !(state = s1 & input = iC)
& !(state = s1 & input = iD)
& !(state = s1 & input = iE)
& !(state = s1 & input = iF)
& !(state = s1 & input = iG)
& !(state = s1 & input = iH)
& !(state = s1 & input = iI)
& !(state = s1 & input = iJ)
& !(state = s10 & input = iC)
& !(state = s10 & input = iD)
& !(state = s10 & input = iE)
& !(state = s10 & input = iF)
& !(state = s10 & input = iG)
& !(state = s10 & input = iH)
& !(state = s10 & input = iI)
& !(state = s10 & input = iJ)
& !(state = s11 & input = iB)
& !(state = s11 & input = iC)
& !(state = s11 & input = iD)
& !(state = s11 & input = iE)
& !(state = s11 & input = iG)
& !(state = s11 & input = iH)
& !(state = s11 & input = iI)
& !(state = s12 & input = iA)
& !(state = s12 & input = iB)
& !(state = s12 & input = iD)
& !(state = s12 & input = iE)
& !(state = s12 & input = iF)
& !(state = s12 & input = iI)
& !(state = s12 & input = iJ)
& !(state = s13 & input = iA)
& !(state = s13 & input = iB)
& !(state = s13 & input = iC)
& !(state = s13 & input = iD)
& !(state = s13 & input = iF)
& !(state = s13 & input = iH)
& !(state = s13 & input = iI)
& !(state = s13 & input = iJ)
& !(state = s14 & input = iA)
& !(state = s14 & input = iC)
& !(state = s14 & input = iD)
& !(state = s14 & input = iE)
& !(state = s14 & input = iF)
& !(state = s14 & input = iH)
& !(state = s14 & input = iI)
& !(state = s14 & input = iJ)
& !(state = s15 & input = iB)
& !(state = s15 & input = iC)
& !(state = s15 & input = iD)
& !(state = s15 & input = iE)
& !(state = s15 & input = iF)
& !(state = s15 & input = iG)
& !(state = s15 & input = iH)
& !(state = s15 & input = iI)
& !(state = s15 & input = iJ)
& !(state = s16 & input = iA)
& !(state = s16 & input = iB)
& !(state = s16 & input = iC)
& !(state = s16 & input = iD)
& !(state = s16 & input = iE)
& !(state = s16 & input = iG)
& !(state = s16 & input = iH)
& !(state = s16 & input = iI)
& !(state = s16 & input = iJ)
& !(state = s17 & input = iA)
& !(state = s17 & input = iB)
& !(state = s17 & input = iC)
& !(state = s17 & input = iE)
& !(state = s17 & input = iF)
& !(state = s17 & input = iG)
& !(state = s17 & input = iH)
& !(state = s17 & input = iI)
& !(state = s17 & input = iJ)
& !(state = s18 & input = iA)
& !(state = s18 & input = iB)
& !(state = s18 & input = iC)
& !(state = s18 & input = iD)
& !(state = s18 & input = iF)
& !(state = s18 & input = iG)
& !(state = s18 & input = iH)
& !(state = s18 & input = iI)
& !(state = s18 & input = iJ)
& !(state = s19 & input = iA)
& !(state = s19 & input = iB)
& !(state = s19 & input = iC)
& !(state = s19 & input = iD)
& !(state = s19 & input = iE)
& !(state = s19 & input = iF)
& !(state = s19 & input = iG)
& !(state = s19 & input = iI)
& !(state = s19 & input = iJ)
& !(state = s2 & input = iB)
& !(state = s2 & input = iC)
& !(state = s2 & input = iD)
& !(state = s2 & input = iE)
& !(state = s2 & input = iF)
& !(state = s2 & input = iG)
& !(state = s2 & input = iH)
& !(state = s2 & input = iI)
& !(state = s2 & input = iJ)
& !(state = s20 & input = iB)
& !(state = s20 & input = iC)
& !(state = s20 & input = iD)
& !(state = s20 & input = iF)
& !(state = s20 & input = iG)
& !(state = s20 & input = iI)
& !(state = s20 & input = iJ)
& !(state = s21 & input = iA)
& !(state = s21 & input = iB)
& !(state = s21 & input = iC)
& !(state = s21 & input = iD)
& !(state = s21 & input = iE)
& !(state = s21 & input = iG)
& !(state = s21 & input = iH)
& !(state = s21 & input = iI)
& !(state = s22 & input = iA)
& !(state = s22 & input = iB)
& !(state = s22 & input = iC)
& !(state = s22 & input = iD)
& !(state = s22 & input = iE)
& !(state = s22 & input = iF)
& !(state = s22 & input = iG)
& !(state = s22 & input = iI)
& !(state = s22 & input = iJ)
& !(state = s23 & input = iA)
& !(state = s23 & input = iB)
& !(state = s23 & input = iC)
& !(state = s23 & input = iD)
& !(state = s23 & input = iE)
& !(state = s23 & input = iF)
& !(state = s23 & input = iG)
& !(state = s23 & input = iI)
& !(state = s23 & input = iJ)
& !(state = s24 & input = iA)
& !(state = s24 & input = iB)
& !(state = s24 & input = iC)
& !(state = s24 & input = iD)
& !(state = s24 & input = iE)
& !(state = s24 & input = iG)
& !(state = s24 & input = iH)
& !(state = s24 & input = iI)
& !(state = s24 & input = iJ)
& !(state = s25 & input = iA)
& !(state = s25 & input = iB)
& !(state = s25 & input = iC)
& !(state = s25 & input = iD)
& !(state = s25 & input = iE)
& !(state = s25 & input = iF)
& !(state = s25 & input = iG)
& !(state = s25 & input = iI)
& !(state = s25 & input = iJ)
& !(state = s3 & input = iA)
& !(state = s3 & input = iC)
& !(state = s3 & input = iD)
& !(state = s3 & input = iE)
& !(state = s3 & input = iF)
& !(state = s3 & input = iG)
& !(state = s3 & input = iH)
& !(state = s3 & input = iI)
& !(state = s3 & input = iJ)
& !(state = s4 & input = iA)
& !(state = s4 & input = iB)
& !(state = s4 & input = iC)
& !(state = s4 & input = iD)
& !(state = s4 & input = iE)
& !(state = s4 & input = iF)
& !(state = s4 & input = iG)
& !(state = s4 & input = iH)
& !(state = s4 & input = iI)
& !(state = s5 & input = iA)
& !(state = s5 & input = iB)
& !(state = s5 & input = iC)
& !(state = s5 & input = iD)
& !(state = s5 & input = iE)
& !(state = s5 & input = iF)
& !(state = s5 & input = iG)
& !(state = s5 & input = iH)
& !(state = s5 & input = iI)
& !(state = s6 & input = iA)
& !(state = s6 & input = iC)
& !(state = s6 & input = iD)
& !(state = s6 & input = iE)
& !(state = s6 & input = iF)
& !(state = s6 & input = iG)
& !(state = s6 & input = iH)
& !(state = s6 & input = iI)
& !(state = s7 & input = iA)
& !(state = s7 & input = iC)
& !(state = s7 & input = iD)
& !(state = s7 & input = iE)
& !(state = s7 & input = iF)
& !(state = s7 & input = iG)
& !(state = s7 & input = iH)
& !(state = s7 & input = iI)
& !(state = s7 & input = iJ)
& !(state = s8 & input = iA)
& !(state = s8 & input = iB)
& !(state = s8 & input = iC)
& !(state = s8 & input = iD)
& !(state = s8 & input = iE)
& !(state = s8 & input = iF)
& !(state = s8 & input = iH)
& !(state = s8 & input = iI)
& !(state = s9 & input = iA)
& !(state = s9 & input = iC)
& !(state = s9 & input = iD)
& !(state = s9 & input = iE)
& !(state = s9 & input = iF)
& !(state = s9 & input = iG)
& !(state = s9 & input = iH)
& !(state = s9 & input = iI)
& !(state = s9 & input = iJ)
LTLSPEC (! (TRUE U (input = iC)) | (! (output = oQ) U ((input = iC) | (((output = oS) & ! (output = oQ)) & X (! (output = oQ) U (output = oY))))))
LTLSPEC (! (TRUE U (output = oZ)) | (! (output = oZ) U (((input = iJ) & ! (output = oZ)) & X (! (output = oZ) U (output = oP)))))
LTLSPEC ((output = oZ) V (! (output = oO) | (output = oZ)))
......
......@@ -534,3 +534,224 @@ ASSIGN
esac;
INVAR !(input = null & output = null)
& !(input != null & output != null)
& !(state = s0 & input = iB)
& !(state = s0 & input = iC)
& !(state = s0 & input = iD)
& !(state = s0 & input = iF)
& !(state = s0 & input = iG)
& !(state = s0 & input = iH)
& !(state = s0 & input = iI)
& !(state = s0 & input = iJ)
& !(state = s1 & input = iB)
& !(state = s1 & input = iC)
& !(state = s1 & input = iD)
& !(state = s1 & input = iE)
& !(state = s1 & input = iF)
& !(state = s1 & input = iG)
& !(state = s1 & input = iH)
& !(state = s1 & input = iI)
& !(state = s1 & input = iJ)
& !(state = s10 & input = iC)
& !(state = s10 & input = iD)
& !(state = s10 & input = iE)
& !(state = s10 & input = iF)
& !(state = s10 & input = iG)
& !(state = s10 & input = iH)
& !(state = s10 & input = iI)
& !(state = s10 & input = iJ)
& !(state = s11 & input = iB)
& !(state = s11 & input = iC)
& !(state = s11 & input = iD)
& !(state = s11 & input = iE)
& !(state = s11 & input = iG)
& !(state = s11 & input = iH)
& !(state = s11 & input = iI)
& !(state = s12 & input = iA)
& !(state = s12 & input = iB)
& !(state = s12 & input = iD)
& !(state = s12 & input = iE)
& !(state = s12 & input = iF)
& !(state = s12 & input = iI)
& !(state = s12 & input = iJ)
& !(state = s13 & input = iA)
& !(state = s13 & input = iB)
& !(state = s13 & input = iC)
& !(state = s13 & input = iD)
& !(state = s13 & input = iF)
& !(state = s13 & input = iH)
& !(state = s13 & input = iI)
& !(state = s13 & input = iJ)
& !(state = s14 & input = iA)
& !(state = s14 & input = iC)
& !(state = s14 & input = iD)
& !(state = s14 & input = iE)
& !(state = s14 & input = iF)
& !(state = s14 & input = iH)
& !(state = s14 & input = iI)
& !(state = s14 & input = iJ)
& !(state = s15 & input = iB)
& !(state = s15 & input = iC)
& !(state = s15 & input = iD)
& !(state = s15 & input = iE)
& !(state = s15 & input = iF)
& !(state = s15 & input = iG)
& !(state = s15 & input = iH)
& !(state = s15 & input = iI)
& !(state = s15 & input = iJ)
& !(state = s16 & input = iA)
& !(state = s16 & input = iB)
& !(state = s16 & input = iC)
& !(state = s16 & input = iD)
& !(state = s16 & input = iE)
& !(state = s16 & input = iG)
& !(state = s16 & input = iH)
& !(state = s16 & input = iI)
& !(state = s16 & input = iJ)
& !(state = s17 & input = iA)
& !(state = s17 & input = iB)
& !(state = s17 & input = iC)
& !(state = s17 & input = iE)
& !(state = s17 & input = iF)
& !(state = s17 & input = iG)
& !(state = s17 & input = iH)
& !(state = s17 & input = iI)
& !(state = s17 & input = iJ)
& !(state = s18 & input = iA)
& !(state = s18 & input = iB)
& !(state = s18 & input = iC)
& !(state = s18 & input = iD)
& !(state = s18 & input = iF)
& !(state = s18 & input = iG)
& !(state = s18 & input = iH)
& !(state = s18 & input = iI)
& !(state = s18 & input = iJ)
& !(state = s19 & input = iA)
& !(state = s19 & input = iB)
& !(state = s19 & input = iC)
& !(state = s19 & input = iD)
& !(state = s19 & input = iE)
& !(state = s19 & input = iF)
& !(state = s19 & input = iG)
& !(state = s19 & input = iI)
& !(state = s19 & input = iJ)
& !(state = s2 & input = iB)
& !(state = s2 & input = iC)
& !(state = s2 & input = iD)
& !(state = s2 & input = iE)
& !(state = s2 & input = iF)
& !(state = s2 & input = iG)
& !(state = s2 & input = iH)
& !(state = s2 & input = iI)
& !(state = s2 & input = iJ)
& !(state = s20 & input = iB)
& !(state = s20 & input = iC)
& !(state = s20 & input = iD)
& !(state = s20 & input = iF)
& !(state = s20 & input = iG)
& !(state = s20 & input = iI)
& !(state = s20 & input = iJ)
& !(state = s21 & input = iA)
& !(state = s21 & input = iB)
& !(state = s21 & input = iC)
& !(state = s21 & input = iD)
& !(state = s21 & input = iE)
& !(state = s21 & input = iG)
& !(state = s21 & input = iH)
& !(state = s21 & input = iI)
& !(state = s22 & input = iA)
& !(state = s22 & input = iB)
& !(state = s22 & input = iC)
& !(state = s22 & input = iD)
& !(state = s22 & input = iE)
& !(state = s22 & input = iF)
& !(state = s22 & input = iG)
& !(state = s22 & input = iI)
& !(state = s22 & input = iJ)
& !(state = s23 & input = iA)
& !(state = s23 & input = iB)
& !(state = s23 & input = iC)
& !(state = s23 & input = iD)
& !(state = s23 & input = iE)
& !(state = s23 & input = iF)
& !(state = s23 & input = iG)
& !(state = s23 & input = iI)
& !(state = s23 & input = iJ)
& !(state = s24 & input = iA)
& !(state = s24 & input = iB)
& !(state = s24 & input = iC)
& !(state = s24 & input = iD)
& !(state = s24 & input = iE)
& !(state = s24 & input = iG)
& !(state = s24 & input = iH)
& !(state = s24 & input = iI)
& !(state = s24 & input = iJ)
& !(state = s25 & input = iA)
& !(state = s25 & input = iB)
& !(state = s25 & input = iC)
& !(state = s25 & input = iD)
& !(state = s25 & input = iE)
& !(state = s25 & input = iF)