@Test public void testLeq() { Assert.assertTrue(ord.isLeq(sb, sb)); Assert.assertTrue(ord.isLeq(sb, s1)); Assert.assertTrue(ord.isLeq(sb, s2)); Assert.assertTrue(ord.isLeq(sb, s3)); Assert.assertTrue(ord.isLeq(sb, st)); Assert.assertFalse(ord.isLeq(s1, sb)); Assert.assertTrue(ord.isLeq(s1, s1)); Assert.assertTrue(ord.isLeq(s1, s2)); Assert.assertFalse(ord.isLeq(s1, s3)); Assert.assertTrue(ord.isLeq(s1, st)); Assert.assertFalse(ord.isLeq(s2, sb)); Assert.assertFalse(ord.isLeq(s2, s1)); Assert.assertTrue(ord.isLeq(s2, s2)); Assert.assertFalse(ord.isLeq(s2, s3)); Assert.assertTrue(ord.isLeq(s2, st)); Assert.assertFalse(ord.isLeq(st, sb)); Assert.assertFalse(ord.isLeq(st, s1)); Assert.assertFalse(ord.isLeq(st, s2)); Assert.assertFalse(ord.isLeq(st, s3)); Assert.assertTrue(ord.isLeq(st, st)); }
@Override public boolean isLeq(final PredState state1, final PredState state2) { try (WithPushPop wpp = new WithPushPop(solver)) { solver.add(PathUtils.unfold(state1.toExpr(), 0)); solver.add(PathUtils.unfold(Not(state2.toExpr()), 0)); return solver.check().isUnsat(); } }
PredOrd implements PartialOrd<PredState> { @Override public boolean isLeq(final PredState state1, final PredState state2) { try (WithPushPop wpp = new WithPushPop(solver)) { solver.add(PathUtils.unfold(state1.toExpr(), 0)); solver.add(PathUtils.unfold(Not(state2.toExpr()), 0)); return solver.check().isUnsat(); } } }
PredOrd implements PartialOrd<PredState> { @Override public boolean isLeq(final PredState state1, final PredState state2) { try (WithPushPop wpp = new WithPushPop(solver)) { solver.add(PathUtils.unfold(state1.toExpr(), 0)); solver.add(PathUtils.unfold(Not(state2.toExpr()), 0)); return solver.check().isUnsat(); } } private  PredOrd(final Solver solver); }
PredOrd implements PartialOrd<PredState> { @Override public boolean isLeq(final PredState state1, final PredState state2) { try (WithPushPop wpp = new WithPushPop(solver)) { solver.add(PathUtils.unfold(state1.toExpr(), 0)); solver.add(PathUtils.unfold(Not(state2.toExpr()), 0)); return solver.check().isUnsat(); } } private  PredOrd(final Solver solver); static PredOrd create(final Solver solver); @Override boolean isLeq(final PredState state1, final PredState state2); }
PredOrd implements PartialOrd<PredState> { @Override public boolean isLeq(final PredState state1, final PredState state2) { try (WithPushPop wpp = new WithPushPop(solver)) { solver.add(PathUtils.unfold(state1.toExpr(), 0)); solver.add(PathUtils.unfold(Not(state2.toExpr()), 0)); return solver.check().isUnsat(); } } private  PredOrd(final Solver solver); static PredOrd create(final Solver solver); @Override boolean isLeq(final PredState state1, final PredState state2);  }