Commit d4eac599 authored by Marek Chalupa's avatar Marek Chalupa
Browse files

bself: allow empty inductive sets 

That simplifies the presentation and does not hurt.
parent acebfe21

slowbeast/bse/bself.py

+5 −5
Original line number Diff line number Diff line
@@ -75,9 +75,9 @@ def _check_set(executor, S, L, target): 
        )

        return False

    # --- workaround ends here...

    if S.is_empty():

        dbg("Starting sequence is empty")

        return False

   #if S.is_empty():

   #    dbg("Starting sequence is empty")

   #    return False

    return True
@@ -111,7 +111,7 @@ def overapprox_state(executor, s, E, target, L): 
    yield from _overapprox_with_assumptions(E, L, S, executor, s, target)



    # try without any relation

    assert not S.is_empty(), "Infeasible states given to overapproximate"

    #assert not S.is_empty(), "Infeasible states given to overapproximate"

    yield overapprox_set(executor, s.expr_manager(), S, E, target, None, L)
@@ -552,7 +552,7 @@ class BSELFChecker(BaseBSE): 
        create_set = self.create_set

        target = seq0[-1]

        S = seq0.as_set().copy()  # we're going to change S

        assert not S.is_empty(), f"Starting sequence is infeasible!: {seq0}"

        #assert not S.is_empty(), f"Starting sequence is infeasible!: {seq0}"

        EM = getGlobalExprManager()



        yielded_seqs = []

slowbeast/kindse/overapproximations.py

+1 −1
Original line number Diff line number Diff line
@@ -795,7 +795,7 @@ def overapprox_set( 
    if assumptions:

        assumptions = assumptions.translated(unsafe)



    assert not S.is_empty(), "Overapproximating empty set"

    #assert not S.is_empty(), "Overapproximating empty set"

    assert intersection(

        S, unsafe

    ).is_empty(), f"Whata? Unsafe states among one-step reachable safe states:\nS = {S},\nunsafe = {unsafe}"

slowbeast/symexe/statesset.py

+4 −4
Original line number Diff line number Diff line
@@ -95,10 +95,10 @@ class StatesSet: 
        newexpr = EM.Or(expr, state.constraints_obj().as_formula(EM))

        if not newexpr.is_concrete():

            C.add(newexpr)

        else:

            # if newexpr is concrete, it must be True. And adding True is useless,

            # its the same as empty constraints

            assert newexpr.value() is True  # this is Or expr...

       #else:

       #    # if newexpr is concrete, it must be True. And adding True is useless,

       #    # its the same as empty constraints

       #    assert newexpr.value() is True  # this is Or expr...

        state.set_constraints(C)



    def model(self):