Skip to content

Commit

Permalink
Enable IC3 property optimization
Browse files Browse the repository at this point in the history
  • Loading branch information
@mondokm
mondokm committed Feb 20, 2025
1 parent 4d85141 commit 7440b35
Show file tree
Hide file tree
Showing 3 changed files with 138 additions and 110 deletions.
2 changes: 1 addition & 1 deletion ...cts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ic3/Ic3Checker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ public Ic3Checker(
true,
true,
true,
false,
true,
logger);
}

Expand Down
244 changes: 136 additions & 108 deletions ...s/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsIc3CheckerTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,46 +50,50 @@ public class XstsIc3CheckerTest {
public static Collection<Object[]> data() {
return Arrays.asList(
new Object[][] {
// {
// "src/test/resources/model/trafficlight.xsts",
// "src/test/resources/property/green_and_red.prop",
// true
// },
// {
// "src/test/resources/model/trafficlight_v2.xsts",
// "src/test/resources/property/green_and_red.prop",
// true
// },
// {
// "src/test/resources/model/counter5.xsts",
// "src/test/resources/property/x_between_0_and_5.prop",
// true
// },
// {
// "src/test/resources/model/counter5.xsts",
// "src/test/resources/property/x_eq_5.prop",
// false
// },
// {
// "src/test/resources/model/x_and_y.xsts",
// "src/test/resources/property/x_geq_y.prop",
// true
// },
// {
// "src/test/resources/model/x_powers.xsts",
// "src/test/resources/property/x_even.prop",
// true
// },
// {
// "src/test/resources/model/cross_with.xsts",
// "src/test/resources/property/cross.prop",
// false
// },
// {
// "src/test/resources/model/cross_without.xsts",
// "src/test/resources/property/cross.prop",
// false
// },
{
"src/test/resources/model/trafficlight.xsts",
"src/test/resources/property/green_and_red.prop",
true
},
{
"src/test/resources/model/trafficlight_v2.xsts",
"src/test/resources/property/green_and_red.prop",
true
},
{
"src/test/resources/model/counter5.xsts",
"src/test/resources/property/x_between_0_and_5.prop",
true
},
{
"src/test/resources/model/counter5.xsts",
"src/test/resources/property/x_eq_5.prop",
false
},
{
"src/test/resources/model/x_and_y.xsts",
"src/test/resources/property/x_geq_y.prop",
true
},
{
"src/test/resources/model/x_powers.xsts",
"src/test/resources/property/x_even.prop",
true
},
// {
//
// "src/test/resources/model/cross_with.xsts",
//
// "src/test/resources/property/cross.prop",
// false
// },
// {
//
// "src/test/resources/model/cross_without.xsts",
//
// "src/test/resources/property/cross.prop",
// false
// },
{
"src/test/resources/model/choices.xsts",
"src/test/resources/property/choices.prop",
Expand Down Expand Up @@ -135,70 +139,92 @@ public static Collection<Object[]> data() {
"src/test/resources/property/x_eq_5.prop",
false
},
// {
// "src/test/resources/model/counter50.xsts",
// "src/test/resources/property/x_eq_50.prop",
// false
// },
// {
// "src/test/resources/model/counter50.xsts",
// "src/test/resources/property/x_eq_51.prop",
// true
// },
// {
// "src/test/resources/model/count_up_down.xsts",
// "src/test/resources/property/count_up_down.prop",
// false
// },
// {
// "src/test/resources/model/count_up_down.xsts",
// "src/test/resources/property/count_up_down2.prop",
// true
// },
// {
// "src/test/resources/model/count_up_down.xsts",
// "src/test/resources/property/count_up_down2.prop",
// true
// },

// {"src/test/resources/model/bhmr2007.xsts",
// "src/test/resources/property/bhmr2007.prop", true},
// {
//
// "src/test/resources/model/counter50.xsts",
//
// "src/test/resources/property/x_eq_50.prop",
// false
// },
// {
//
// "src/test/resources/model/counter50.xsts",
//
// "src/test/resources/property/x_eq_51.prop",
// true
// },
// {
//
// "src/test/resources/model/count_up_down.xsts",
//
// "src/test/resources/property/count_up_down.prop",
// false
// },
// {
//
// "src/test/resources/model/count_up_down.xsts",
//
// "src/test/resources/property/count_up_down2.prop",
// true
// },
// {
//
// "src/test/resources/model/count_up_down.xsts",
//
// "src/test/resources/property/count_up_down2.prop",
// true
// },

// {
// "src/test/resources/model/css2003.xsts",
// "src/test/resources/property/css2003.prop",
// true
// },
// {
// "src/test/resources/model/array_counter.xsts",
// "src/test/resources/property/array_10.prop",
// false
// },
// {
// "src/test/resources/model/array_constant.xsts",
// "src/test/resources/property/array_constant.prop",
// true
// },
// {
// "src/test/resources/model/localvars.xsts",
// "src/test/resources/property/localvars.prop",
// true
// },
// {
// "src/test/resources/model/localvars2.xsts",
// "src/test/resources/property/localvars2.prop",
// true
// },
// {
// "src/test/resources/model/loopxy.xsts",
// "src/test/resources/property/loopxy.prop",
// true
// },
// {
// "src/test/resources/model/arraywrite_sugar.xsts",
// "src/test/resources/property/arraywrite_sugar.prop",
// false
// },
//
// {"src/test/resources/model/bhmr2007.xsts",
//
// "src/test/resources/property/bhmr2007.prop", true},
//
// {
//
// "src/test/resources/model/css2003.xsts",
//
// "src/test/resources/property/css2003.prop",
// true
// },
// {
//
// "src/test/resources/model/array_counter.xsts",
//
// "src/test/resources/property/array_10.prop",
// false
// },
// {
//
// "src/test/resources/model/array_constant.xsts",
//
// "src/test/resources/property/array_constant.prop",
// true
// },
{
"src/test/resources/model/localvars.xsts",
"src/test/resources/property/localvars.prop",
true
},
{
"src/test/resources/model/localvars2.xsts",
"src/test/resources/property/localvars2.prop",
true
},
// {
//
// "src/test/resources/model/loopxy.xsts",
//
// "src/test/resources/property/loopxy.prop",
// true
// },
// {
//
// "src/test/resources/model/arraywrite_sugar.xsts",
//
// "src/test/resources/property/arraywrite_sugar.prop",
// false
// },
// {
// "src/test/resources/model/if1.xsts",
// "src/test/resources/property/if1.prop",
Expand All @@ -209,11 +235,13 @@ public static Collection<Object[]> data() {
// "src/test/resources/property/if2.prop",
// false
// },
// {
// "src/test/resources/model/localvars3.xsts",
// "src/test/resources/property/localvars3.prop",
// false
// },
// {
//
// "src/test/resources/model/localvars3.xsts",
//
// "src/test/resources/property/localvars3.prop",
// false
// },
{
"src/test/resources/model/bool.xsts",
"src/test/resources/property/bool.prop",
Expand Down
2 changes: 1 addition & 1 deletion subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliIC3.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ class XstsCliIC3 :
notBOpt,
propagateOpt,
filterOpt,
false,
true,
logger,
)
val result = checker.check()
Expand Down

0 comments on commit 7440b35

Please sign in to comment.