class StateMachineChecker::CTL::EG
The existential universal operator.
Public Instance Methods
check(model)
click to toggle source
Check which states of the model have a path for which the subformula is always satisfied
@param [LabeledMachine] model @return [CheckResult]
# File lib/state_machine_checker/ctl/e_g.rb, line 10 def check(model) subresult = subformula.check(model) projection = subformula_projection(model, subresult) scc = strongly_connected_components(projection) # Components must have more than one element, a self loop, or no # transitions in the original fsm. # TODO: this being necessary probably means we're doing something wrong. scc.select! do |states| states.length > 1 || begin c = states.first transitions = model.transitions_from(c) transitions.empty? || transitions.any? { |t| t.to == c } end end build_check_result(scc, model, projection) end
to_s()
click to toggle source
# File lib/state_machine_checker/ctl/e_g.rb, line 32 def to_s "EG(#{subformula})" end
Private Instance Methods
assign(s, root, assigned, assignments, projection)
click to toggle source
# File lib/state_machine_checker/ctl/e_g.rb, line 123 def assign(s, root, assigned, assignments, projection) unless assigned.include?(s) assigned << s if assignments[root].nil? assignments[root] = Set.new end assignments[root] << s projection.transitions_to(s).each do |transition| assign(transition.from, root, assigned, assignments, projection) end end end
build_check_result(scc, model, projection)
click to toggle source
# File lib/state_machine_checker/ctl/e_g.rb, line 66 def build_check_result(scc, model, projection) # Initialize hash with every state unsatisfied. result = model.states.each_with_object({}) { |s, h| h[s] = StateResult.new(false, []) } scc.each do |component_states| # For each state of the component search backwards. component_states.each do |state| loop_witness = scc_loop(component_states, state, projection) projection.traverse(state, reverse: true) do |s, transitions| # Ignore other states in the component. if s == state || !component_states.include?(s) result[s] = StateResult.new(true, transitions + loop_witness) else false end end end end CheckResult.new(result) end
scc_loop(component_states, start, model)
click to toggle source
Find a series of transitions within the component_states which start and end with the given state.
# File lib/state_machine_checker/ctl/e_g.rb, line 93 def scc_loop(component_states, start, model) model.traverse(start) do |state, path| # Only search within the component states. if component_states.include?(state) transitions = model.transitions_from(state) to_start = transitions.find { |t| t.to == start } if to_start return path.push(to_start.name) else true # continue end else false end end [] end
strongly_connected_components(projection)
click to toggle source
Implements Kosaraju's algorithm.
# File lib/state_machine_checker/ctl/e_g.rb, line 49 def strongly_connected_components(projection) visited = Set.new l = [] projection.states.each do |s| visit(s, visited, l, projection) end assigned = Set.new assignments = {} # root -> set of states in component l.reverse_each do |s| assign(s, s, assigned, assignments, projection) end assignments.values end
subformula_projection(model, subresult)
click to toggle source
A graph containing only states for which the subformula is true.
# File lib/state_machine_checker/ctl/e_g.rb, line 39 def subformula_projection(model, subresult) transitions = model.transitions.select { |t| subresult.for_state(t.from).satisfied? && subresult.for_state(t.to).satisfied? } FiniteStateMachine.new(model.initial_state, transitions) end
visit(s, visited, l, projection)
click to toggle source
# File lib/state_machine_checker/ctl/e_g.rb, line 113 def visit(s, visited, l, projection) unless visited.include?(s) visited << s projection.transitions_from(s).each do |transition| visit(transition.to, visited, l, projection) end l << s end end