Skip to content

Commit

Permalink
added bencharks for fairness, stability and gr1
Browse files Browse the repository at this point in the history
  • Loading branch information
@Shufang-Zhu
Shufang-Zhu committed Jan 23, 2024
1 parent eb14f96 commit 529cc25
Show file tree
Hide file tree
Showing 243 changed files with 24,920 additions and 45 deletions.
29 changes: 0 additions & 29 deletions example/GR1benchmarks/finding_nemo_agn_goal.tlsf
View file

This file was deleted.

1 change: 0 additions & 1 deletion example/GR1benchmarks/finding_nemo_agn_safety.ltlf
View file

This file was deleted.

1 change: 0 additions & 1 deletion example/GR1benchmarks/finding_nemo_env_safety.ltlf
View file

This file was deleted.

24 changes: 24 additions & 0 deletions example/TLSF/FairnessStability/counter/counter_1.tlsf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
INFO {
TITLE: "counter_1"
DESCRIPTION: "counter_F"
SEMANTICS: Finite,Moore
TARGET: Moore
}

MAIN {

INPUTS {
add;
}

OUTPUTS {
c0;
c1;
b0;
}

GUARANTEES {
((((!(c0)) && (!(b0))) && (G((!(add)) -> (!(X[!](c0))))) && (G(((((!(c0)) && (!(b0))) -> (!(X[!](!((!(b0)) && (!(c1))))))) && (((!(c0)) && b0) -> (!(X[!](!((b0) && (!(c1))))))) && (((c0) && (!(b0))) -> (!(X[!](!((b0) && (!(c1))))))) && (((c0) && b0) -> (!(X[!](!((!(b0)) && (c1)))))))))) && (F(b0)));
}

}
42 changes: 42 additions & 0 deletions example/TLSF/FairnessStability/counter/counter_10.tlsf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
INFO {
TITLE: "counter_10"
DESCRIPTION: "counter_F"
SEMANTICS: Finite,Moore
TARGET: Moore
}

MAIN {

INPUTS {
add;
}

OUTPUTS {
c0;
c1;
c2;
c3;
c4;
c5;
c6;
c7;
c8;
c9;
c10;
b0;
b1;
b2;
b3;
b4;
b5;
b6;
b7;
b8;
b9;
}

GUARANTEES {
((((!(c0)) && (!(c1)) && (!(c2)) && (!(c3)) && (!(c4)) && (!(c5)) && (!(c6)) && (!(c7)) && (!(c8)) && (!(c9)) && (!(b0)) && (!(b1)) && (!(b2)) && (!(b3)) && (!(b4)) && (!(b5)) && (!(b6)) && (!(b7)) && (!(b8)) && (!(b9))) && (G((!(add)) -> (!(X[!](c0))))) && (G(((((!(c0)) && (!(b0))) -> (!(X[!](!((!(b0)) && (!(c1))))))) && (((!(c0)) && b0) -> (!(X[!](!((b0) && (!(c1))))))) && (((c0) && (!(b0))) -> (!(X[!](!((b0) && (!(c1))))))) && (((c0) && b0) -> (!(X[!](!((!(b0)) && (c1)))))))&& ((((!(c1)) && (!(b1))) -> (!(X[!](!((!(b1)) && (!(c2))))))) && (((!(c1)) && b1) -> (!(X[!](!((b1) && (!(c2))))))) && (((c1) && (!(b1))) -> (!(X[!](!((b1) && (!(c2))))))) && (((c1) && b1) -> (!(X[!](!((!(b1)) && (c2)))))))&& ((((!(c2)) && (!(b2))) -> (!(X[!](!((!(b2)) && (!(c3))))))) && (((!(c2)) && b2) -> (!(X[!](!((b2) && (!(c3))))))) && (((c2) && (!(b2))) -> (!(X[!](!((b2) && (!(c3))))))) && (((c2) && b2) -> (!(X[!](!((!(b2)) && (c3)))))))&& ((((!(c3)) && (!(b3))) -> (!(X[!](!((!(b3)) && (!(c4))))))) && (((!(c3)) && b3) -> (!(X[!](!((b3) && (!(c4))))))) && (((c3) && (!(b3))) -> (!(X[!](!((b3) && (!(c4))))))) && (((c3) && b3) -> (!(X[!](!((!(b3)) && (c4)))))))&& ((((!(c4)) && (!(b4))) -> (!(X[!](!((!(b4)) && (!(c5))))))) && (((!(c4)) && b4) -> (!(X[!](!((b4) && (!(c5))))))) && (((c4) && (!(b4))) -> (!(X[!](!((b4) && (!(c5))))))) && (((c4) && b4) -> (!(X[!](!((!(b4)) && (c5)))))))&& ((((!(c5)) && (!(b5))) -> (!(X[!](!((!(b5)) && (!(c6))))))) && (((!(c5)) && b5) -> (!(X[!](!((b5) && (!(c6))))))) && (((c5) && (!(b5))) -> (!(X[!](!((b5) && (!(c6))))))) && (((c5) && b5) -> (!(X[!](!((!(b5)) && (c6)))))))&& ((((!(c6)) && (!(b6))) -> (!(X[!](!((!(b6)) && (!(c7))))))) && (((!(c6)) && b6) -> (!(X[!](!((b6) && (!(c7))))))) && (((c6) && (!(b6))) -> (!(X[!](!((b6) && (!(c7))))))) && (((c6) && b6) -> (!(X[!](!((!(b6)) && (c7)))))))&& ((((!(c7)) && (!(b7))) -> (!(X[!](!((!(b7)) && (!(c8))))))) && (((!(c7)) && b7) -> (!(X[!](!((b7) && (!(c8))))))) && (((c7) && (!(b7))) -> (!(X[!](!((b7) && (!(c8))))))) && (((c7) && b7) -> (!(X[!](!((!(b7)) && (c8)))))))&& ((((!(c8)) && (!(b8))) -> (!(X[!](!((!(b8)) && (!(c9))))))) && (((!(c8)) && b8) -> (!(X[!](!((b8) && (!(c9))))))) && (((c8) && (!(b8))) -> (!(X[!](!((b8) && (!(c9))))))) && (((c8) && b8) -> (!(X[!](!((!(b8)) && (c9)))))))&& ((((!(c9)) && (!(b9))) -> (!(X[!](!((!(b9)) && (!(c10))))))) && (((!(c9)) && b9) -> (!(X[!](!((b9) && (!(c10))))))) && (((c9) && (!(b9))) -> (!(X[!](!((b9) && (!(c10))))))) && (((c9) && b9) -> (!(X[!](!((!(b9)) && (c10)))))))))) && (F(b0 && (b1) && (b2) && (b3) && (b4) && (b5) && (b6) && (b7) && (b8) && (b9))));
}

}
222 changes: 222 additions & 0 deletions example/TLSF/FairnessStability/counter/counter_100.tlsf
View file

Large diffs are not rendered by default.

44 changes: 44 additions & 0 deletions example/TLSF/FairnessStability/counter/counter_11.tlsf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
INFO {
TITLE: "counter_11"
DESCRIPTION: "counter_F"
SEMANTICS: Finite,Moore
TARGET: Moore
}

MAIN {

INPUTS {
add;
}

OUTPUTS {
c0;
c1;
c2;
c3;
c4;
c5;
c6;
c7;
c8;
c9;
c10;
c11;
b0;
b1;
b2;
b3;
b4;
b5;
b6;
b7;
b8;
b9;
b10;
}

GUARANTEES {
((((!(c0)) && (!(c1)) && (!(c2)) && (!(c3)) && (!(c4)) && (!(c5)) && (!(c6)) && (!(c7)) && (!(c8)) && (!(c9)) && (!(c10)) && (!(b0)) && (!(b1)) && (!(b2)) && (!(b3)) && (!(b4)) && (!(b5)) && (!(b6)) && (!(b7)) && (!(b8)) && (!(b9)) && (!(b10))) && (G((!(add)) -> (!(X[!](c0))))) && (G(((((!(c0)) && (!(b0))) -> (!(X[!](!((!(b0)) && (!(c1))))))) && (((!(c0)) && b0) -> (!(X[!](!((b0) && (!(c1))))))) && (((c0) && (!(b0))) -> (!(X[!](!((b0) && (!(c1))))))) && (((c0) && b0) -> (!(X[!](!((!(b0)) && (c1)))))))&& ((((!(c1)) && (!(b1))) -> (!(X[!](!((!(b1)) && (!(c2))))))) && (((!(c1)) && b1) -> (!(X[!](!((b1) && (!(c2))))))) && (((c1) && (!(b1))) -> (!(X[!](!((b1) && (!(c2))))))) && (((c1) && b1) -> (!(X[!](!((!(b1)) && (c2)))))))&& ((((!(c2)) && (!(b2))) -> (!(X[!](!((!(b2)) && (!(c3))))))) && (((!(c2)) && b2) -> (!(X[!](!((b2) && (!(c3))))))) && (((c2) && (!(b2))) -> (!(X[!](!((b2) && (!(c3))))))) && (((c2) && b2) -> (!(X[!](!((!(b2)) && (c3)))))))&& ((((!(c3)) && (!(b3))) -> (!(X[!](!((!(b3)) && (!(c4))))))) && (((!(c3)) && b3) -> (!(X[!](!((b3) && (!(c4))))))) && (((c3) && (!(b3))) -> (!(X[!](!((b3) && (!(c4))))))) && (((c3) && b3) -> (!(X[!](!((!(b3)) && (c4)))))))&& ((((!(c4)) && (!(b4))) -> (!(X[!](!((!(b4)) && (!(c5))))))) && (((!(c4)) && b4) -> (!(X[!](!((b4) && (!(c5))))))) && (((c4) && (!(b4))) -> (!(X[!](!((b4) && (!(c5))))))) && (((c4) && b4) -> (!(X[!](!((!(b4)) && (c5)))))))&& ((((!(c5)) && (!(b5))) -> (!(X[!](!((!(b5)) && (!(c6))))))) && (((!(c5)) && b5) -> (!(X[!](!((b5) && (!(c6))))))) && (((c5) && (!(b5))) -> (!(X[!](!((b5) && (!(c6))))))) && (((c5) && b5) -> (!(X[!](!((!(b5)) && (c6)))))))&& ((((!(c6)) && (!(b6))) -> (!(X[!](!((!(b6)) && (!(c7))))))) && (((!(c6)) && b6) -> (!(X[!](!((b6) && (!(c7))))))) && (((c6) && (!(b6))) -> (!(X[!](!((b6) && (!(c7))))))) && (((c6) && b6) -> (!(X[!](!((!(b6)) && (c7)))))))&& ((((!(c7)) && (!(b7))) -> (!(X[!](!((!(b7)) && (!(c8))))))) && (((!(c7)) && b7) -> (!(X[!](!((b7) && (!(c8))))))) && (((c7) && (!(b7))) -> (!(X[!](!((b7) && (!(c8))))))) && (((c7) && b7) -> (!(X[!](!((!(b7)) && (c8)))))))&& ((((!(c8)) && (!(b8))) -> (!(X[!](!((!(b8)) && (!(c9))))))) && (((!(c8)) && b8) -> (!(X[!](!((b8) && (!(c9))))))) && (((c8) && (!(b8))) -> (!(X[!](!((b8) && (!(c9))))))) && (((c8) && b8) -> (!(X[!](!((!(b8)) && (c9)))))))&& ((((!(c9)) && (!(b9))) -> (!(X[!](!((!(b9)) && (!(c10))))))) && (((!(c9)) && b9) -> (!(X[!](!((b9) && (!(c10))))))) && (((c9) && (!(b9))) -> (!(X[!](!((b9) && (!(c10))))))) && (((c9) && b9) -> (!(X[!](!((!(b9)) && (c10)))))))&& ((((!(c10)) && (!(b10))) -> (!(X[!](!((!(b10)) && (!(c11))))))) && (((!(c10)) && b10) -> (!(X[!](!((b10) && (!(c11))))))) && (((c10) && (!(b10))) -> (!(X[!](!((b10) && (!(c11))))))) && (((c10) && b10) -> (!(X[!](!((!(b10)) && (c11)))))))))) && (F(b0 && (b1) && (b2) && (b3) && (b4) && (b5) && (b6) && (b7) && (b8) && (b9) && (b10))));
}

}
46 changes: 46 additions & 0 deletions example/TLSF/FairnessStability/counter/counter_12.tlsf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
INFO {
TITLE: "counter_12"
DESCRIPTION: "counter_F"
SEMANTICS: Finite,Moore
TARGET: Moore
}

MAIN {

INPUTS {
add;
}

OUTPUTS {
c0;
c1;
c2;
c3;
c4;
c5;
c6;
c7;
c8;
c9;
c10;
c11;
c12;
b0;
b1;
b2;
b3;
b4;
b5;
b6;
b7;
b8;
b9;
b10;
b11;
}

GUARANTEES {
((((!(c0)) && (!(c1)) && (!(c2)) && (!(c3)) && (!(c4)) && (!(c5)) && (!(c6)) && (!(c7)) && (!(c8)) && (!(c9)) && (!(c10)) && (!(c11)) && (!(b0)) && (!(b1)) && (!(b2)) && (!(b3)) && (!(b4)) && (!(b5)) && (!(b6)) && (!(b7)) && (!(b8)) && (!(b9)) && (!(b10)) && (!(b11))) && (G((!(add)) -> (!(X[!](c0))))) && (G(((((!(c0)) && (!(b0))) -> (!(X[!](!((!(b0)) && (!(c1))))))) && (((!(c0)) && b0) -> (!(X[!](!((b0) && (!(c1))))))) && (((c0) && (!(b0))) -> (!(X[!](!((b0) && (!(c1))))))) && (((c0) && b0) -> (!(X[!](!((!(b0)) && (c1)))))))&& ((((!(c1)) && (!(b1))) -> (!(X[!](!((!(b1)) && (!(c2))))))) && (((!(c1)) && b1) -> (!(X[!](!((b1) && (!(c2))))))) && (((c1) && (!(b1))) -> (!(X[!](!((b1) && (!(c2))))))) && (((c1) && b1) -> (!(X[!](!((!(b1)) && (c2)))))))&& ((((!(c2)) && (!(b2))) -> (!(X[!](!((!(b2)) && (!(c3))))))) && (((!(c2)) && b2) -> (!(X[!](!((b2) && (!(c3))))))) && (((c2) && (!(b2))) -> (!(X[!](!((b2) && (!(c3))))))) && (((c2) && b2) -> (!(X[!](!((!(b2)) && (c3)))))))&& ((((!(c3)) && (!(b3))) -> (!(X[!](!((!(b3)) && (!(c4))))))) && (((!(c3)) && b3) -> (!(X[!](!((b3) && (!(c4))))))) && (((c3) && (!(b3))) -> (!(X[!](!((b3) && (!(c4))))))) && (((c3) && b3) -> (!(X[!](!((!(b3)) && (c4)))))))&& ((((!(c4)) && (!(b4))) -> (!(X[!](!((!(b4)) && (!(c5))))))) && (((!(c4)) && b4) -> (!(X[!](!((b4) && (!(c5))))))) && (((c4) && (!(b4))) -> (!(X[!](!((b4) && (!(c5))))))) && (((c4) && b4) -> (!(X[!](!((!(b4)) && (c5)))))))&& ((((!(c5)) && (!(b5))) -> (!(X[!](!((!(b5)) && (!(c6))))))) && (((!(c5)) && b5) -> (!(X[!](!((b5) && (!(c6))))))) && (((c5) && (!(b5))) -> (!(X[!](!((b5) && (!(c6))))))) && (((c5) && b5) -> (!(X[!](!((!(b5)) && (c6)))))))&& ((((!(c6)) && (!(b6))) -> (!(X[!](!((!(b6)) && (!(c7))))))) && (((!(c6)) && b6) -> (!(X[!](!((b6) && (!(c7))))))) && (((c6) && (!(b6))) -> (!(X[!](!((b6) && (!(c7))))))) && (((c6) && b6) -> (!(X[!](!((!(b6)) && (c7)))))))&& ((((!(c7)) && (!(b7))) -> (!(X[!](!((!(b7)) && (!(c8))))))) && (((!(c7)) && b7) -> (!(X[!](!((b7) && (!(c8))))))) && (((c7) && (!(b7))) -> (!(X[!](!((b7) && (!(c8))))))) && (((c7) && b7) -> (!(X[!](!((!(b7)) && (c8)))))))&& ((((!(c8)) && (!(b8))) -> (!(X[!](!((!(b8)) && (!(c9))))))) && (((!(c8)) && b8) -> (!(X[!](!((b8) && (!(c9))))))) && (((c8) && (!(b8))) -> (!(X[!](!((b8) && (!(c9))))))) && (((c8) && b8) -> (!(X[!](!((!(b8)) && (c9)))))))&& ((((!(c9)) && (!(b9))) -> (!(X[!](!((!(b9)) && (!(c10))))))) && (((!(c9)) && b9) -> (!(X[!](!((b9) && (!(c10))))))) && (((c9) && (!(b9))) -> (!(X[!](!((b9) && (!(c10))))))) && (((c9) && b9) -> (!(X[!](!((!(b9)) && (c10)))))))&& ((((!(c10)) && (!(b10))) -> (!(X[!](!((!(b10)) && (!(c11))))))) && (((!(c10)) && b10) -> (!(X[!](!((b10) && (!(c11))))))) && (((c10) && (!(b10))) -> (!(X[!](!((b10) && (!(c11))))))) && (((c10) && b10) -> (!(X[!](!((!(b10)) && (c11)))))))&& ((((!(c11)) && (!(b11))) -> (!(X[!](!((!(b11)) && (!(c12))))))) && (((!(c11)) && b11) -> (!(X[!](!((b11) && (!(c12))))))) && (((c11) && (!(b11))) -> (!(X[!](!((b11) && (!(c12))))))) && (((c11) && b11) -> (!(X[!](!((!(b11)) && (c12)))))))))) && (F(b0 && (b1) && (b2) && (b3) && (b4) && (b5) && (b6) && (b7) && (b8) && (b9) && (b10) && (b11))));
}

}
48 changes: 48 additions & 0 deletions example/TLSF/FairnessStability/counter/counter_13.tlsf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
INFO {
TITLE: "counter_13"
DESCRIPTION: "counter_F"
SEMANTICS: Finite,Moore
TARGET: Moore
}

MAIN {

INPUTS {
add;
}

OUTPUTS {
c0;
c1;
c2;
c3;
c4;
c5;
c6;
c7;
c8;
c9;
c10;
c11;
c12;
c13;
b0;
b1;
b2;
b3;
b4;
b5;
b6;
b7;
b8;
b9;
b10;
b11;
b12;
}

GUARANTEES {
((((!(c0)) && (!(c1)) && (!(c2)) && (!(c3)) && (!(c4)) && (!(c5)) && (!(c6)) && (!(c7)) && (!(c8)) && (!(c9)) && (!(c10)) && (!(c11)) && (!(c12)) && (!(b0)) && (!(b1)) && (!(b2)) && (!(b3)) && (!(b4)) && (!(b5)) && (!(b6)) && (!(b7)) && (!(b8)) && (!(b9)) && (!(b10)) && (!(b11)) && (!(b12))) && (G((!(add)) -> (!(X[!](c0))))) && (G(((((!(c0)) && (!(b0))) -> (!(X[!](!((!(b0)) && (!(c1))))))) && (((!(c0)) && b0) -> (!(X[!](!((b0) && (!(c1))))))) && (((c0) && (!(b0))) -> (!(X[!](!((b0) && (!(c1))))))) && (((c0) && b0) -> (!(X[!](!((!(b0)) && (c1)))))))&& ((((!(c1)) && (!(b1))) -> (!(X[!](!((!(b1)) && (!(c2))))))) && (((!(c1)) && b1) -> (!(X[!](!((b1) && (!(c2))))))) && (((c1) && (!(b1))) -> (!(X[!](!((b1) && (!(c2))))))) && (((c1) && b1) -> (!(X[!](!((!(b1)) && (c2)))))))&& ((((!(c2)) && (!(b2))) -> (!(X[!](!((!(b2)) && (!(c3))))))) && (((!(c2)) && b2) -> (!(X[!](!((b2) && (!(c3))))))) && (((c2) && (!(b2))) -> (!(X[!](!((b2) && (!(c3))))))) && (((c2) && b2) -> (!(X[!](!((!(b2)) && (c3)))))))&& ((((!(c3)) && (!(b3))) -> (!(X[!](!((!(b3)) && (!(c4))))))) && (((!(c3)) && b3) -> (!(X[!](!((b3) && (!(c4))))))) && (((c3) && (!(b3))) -> (!(X[!](!((b3) && (!(c4))))))) && (((c3) && b3) -> (!(X[!](!((!(b3)) && (c4)))))))&& ((((!(c4)) && (!(b4))) -> (!(X[!](!((!(b4)) && (!(c5))))))) && (((!(c4)) && b4) -> (!(X[!](!((b4) && (!(c5))))))) && (((c4) && (!(b4))) -> (!(X[!](!((b4) && (!(c5))))))) && (((c4) && b4) -> (!(X[!](!((!(b4)) && (c5)))))))&& ((((!(c5)) && (!(b5))) -> (!(X[!](!((!(b5)) && (!(c6))))))) && (((!(c5)) && b5) -> (!(X[!](!((b5) && (!(c6))))))) && (((c5) && (!(b5))) -> (!(X[!](!((b5) && (!(c6))))))) && (((c5) && b5) -> (!(X[!](!((!(b5)) && (c6)))))))&& ((((!(c6)) && (!(b6))) -> (!(X[!](!((!(b6)) && (!(c7))))))) && (((!(c6)) && b6) -> (!(X[!](!((b6) && (!(c7))))))) && (((c6) && (!(b6))) -> (!(X[!](!((b6) && (!(c7))))))) && (((c6) && b6) -> (!(X[!](!((!(b6)) && (c7)))))))&& ((((!(c7)) && (!(b7))) -> (!(X[!](!((!(b7)) && (!(c8))))))) && (((!(c7)) && b7) -> (!(X[!](!((b7) && (!(c8))))))) && (((c7) && (!(b7))) -> (!(X[!](!((b7) && (!(c8))))))) && (((c7) && b7) -> (!(X[!](!((!(b7)) && (c8)))))))&& ((((!(c8)) && (!(b8))) -> (!(X[!](!((!(b8)) && (!(c9))))))) && (((!(c8)) && b8) -> (!(X[!](!((b8) && (!(c9))))))) && (((c8) && (!(b8))) -> (!(X[!](!((b8) && (!(c9))))))) && (((c8) && b8) -> (!(X[!](!((!(b8)) && (c9)))))))&& ((((!(c9)) && (!(b9))) -> (!(X[!](!((!(b9)) && (!(c10))))))) && (((!(c9)) && b9) -> (!(X[!](!((b9) && (!(c10))))))) && (((c9) && (!(b9))) -> (!(X[!](!((b9) && (!(c10))))))) && (((c9) && b9) -> (!(X[!](!((!(b9)) && (c10)))))))&& ((((!(c10)) && (!(b10))) -> (!(X[!](!((!(b10)) && (!(c11))))))) && (((!(c10)) && b10) -> (!(X[!](!((b10) && (!(c11))))))) && (((c10) && (!(b10))) -> (!(X[!](!((b10) && (!(c11))))))) && (((c10) && b10) -> (!(X[!](!((!(b10)) && (c11)))))))&& ((((!(c11)) && (!(b11))) -> (!(X[!](!((!(b11)) && (!(c12))))))) && (((!(c11)) && b11) -> (!(X[!](!((b11) && (!(c12))))))) && (((c11) && (!(b11))) -> (!(X[!](!((b11) && (!(c12))))))) && (((c11) && b11) -> (!(X[!](!((!(b11)) && (c12)))))))&& ((((!(c12)) && (!(b12))) -> (!(X[!](!((!(b12)) && (!(c13))))))) && (((!(c12)) && b12) -> (!(X[!](!((b12) && (!(c13))))))) && (((c12) && (!(b12))) -> (!(X[!](!((b12) && (!(c13))))))) && (((c12) && b12) -> (!(X[!](!((!(b12)) && (c13)))))))))) && (F(b0 && (b1) && (b2) && (b3) && (b4) && (b5) && (b6) && (b7) && (b8) && (b9) && (b10) && (b11) && (b12))));
}

}
Loading

0 comments on commit 529cc25

Please sign in to comment.