157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
|
# File 'lib/bparity/formal/lts.rb', line 157
def compare(old_lts, new_lts, relation: :trace, assumptions: %i[h1 h6 h7], exact: true)
unless %i[trace bisim].include?(relation.to_sym)
raise ConfigurationError, "Unsupported LTS relation #{relation}. Use trace or bisim."
end
unless old_lts.deterministic? && new_lts.deterministic?
return Result.new(level: :f3, verdict: :inconclusive,
scope: Scope.new(size: [old_lts.states.length, new_lts.states.length].max,
depth: nil, cases: 0, exhaustive: false),
assumptions:, out_of_scope: ["nondeterministic model equivalence"],
details: details(old_lts, new_lts, relation, false).merge(
"reason" => "The built-in F3 checker requires deterministic LTS models."
))
end
counterexample = distinguishing_sequence(old_lts, new_lts)
verdict = if counterexample then :difference_found
elsif exact then :no_difference_found
else :inconclusive
end
Result.new(level: :f3, verdict:,
scope: Scope.new(size: [old_lts.states.length, new_lts.states.length].max,
depth: nil, cases: visited_count, exhaustive: exact),
assumptions:, out_of_scope: ["operations outside the learned alphabet", "unprojected state"],
counterexample: counterexample && { "sequence" => counterexample },
details: details(old_lts, new_lts, relation, exact))
end
|