Skip to content

Commit

Permalink
fix #113. The ReachabilityResult needs to return an array of reachabl…
Browse files Browse the repository at this point in the history
…e sets instead of one set in the form of AbstractPolytope.
  • Loading branch information
changliuliu committed Jul 12, 2020
1 parent a2fff4c commit 16d5522
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/satisfiability/bab.jl
Original file line number Diff line number Diff line change
Expand Up @@ -39,13 +39,14 @@ function solve(solver::BaB, problem::Problem)
return interpret_result(reach, bound, problem.output, x_l, x_u)
end

# This function is used by BaB and Sherlock
function interpret_result(reach, bound, output, x_l, x_u)
if high(reach) < high(output) && low(reach) > low(output)
return ReachabilityResult(:holds, [reach])
end
high(bound) > high(output) && return CounterExampleResult(:violated, x_u)
low(bound) < low(output) && return CounterExampleResult(:violated, x_l)
return ReachabilityResult(:unknown, reach)
return ReachabilityResult(:unknown, [reach])
end

function output_bound(solver::BaB, problem::Problem, type::Symbol)
Expand Down

0 comments on commit 16d5522

Please sign in to comment.