check(f:Formula, p:Instruction, s:State) : Formula

• case p = {q₁ ; q₂ ; ... ; q_m} ; p₂ ; ... ; p_n:
  • check(f, q₁ ; q₂ ; ... ; q_m ; p₂ ; ... ; p_n, s) flattening nested instruction blocks
• case p = {q₁ || q₂ || ... || q_m} ; p₂ ; ... ; p_n:
  • check(f, {q₁ ; p₂ ; ... ; p_n} || {q₂ ; p₂ ; ... ; p_n} || ... || {q_m ; p₂ ; ... ; p_n}, s) flattening nested instruction blocks
• case p = p₁ ; p₂ ; ... ; p_n:
  • s' = execute p₁ in state s
  • if s' is a failing state, then return f which is true.
  • otherwise:
    • if eval_seq(f,s') yields true or false, then return f with the corresponding value.
    • else check(f,p,s'), i.e. continue execution.
• case p = q₁ || q₂ || ... || q_m:
  • for each q in {q₁, q₂, ... , q_m}
    • if f = EF(_) or f = EG(_) and check(f,q,s) is true, then return f which is true
    • if f = AF(_) or f = AG(_) and check(f,q,s) is not true, then return f which is false
  • if f = EF(_) or f = EG(_) return false no branch yielded true
  • if f = AF(_) or f = AG(_) return true no branch yielded false
• case p = _ //some instruction//
  • if f = XY(f') where X is any path quantifier and Y is any temporal operator, then check(f',p,s) strip temporal part and check formula
  • if f contains boolean operators, proceed similarly to eval_seq
  • s' = execute p in state s
  • if s' is a failing state, then return f which is true.
  • otherwise return false.

eval_seq( f : Formula, s : State) : Formula

• case f = AG(f') or EG(f')
  • if eval_seq(f',s) is False, then return f which is false.
  • otherwise, if f' is pending, then f would be true in this state if it is true in a next state. Also, if f' is true, we still need to check it in the next state (due to the temporal operator G), which amounts to checking f in the next state. Hence return f which is pending.
• case f = AF(f') or EF(f')
  • if eval_seq(f',s) is True, then return f which is true.
  • otherwise, if f' is pending, then f would be true in this state if it is true in a next state. Also, if f' is false, we need to check it in the next state (due to the temporal operator F), which amounts to checking f in the next state. Hence return f which is pending.
• case f is f₁ AND f₂
  • if eval_seq(f₁,s) is true and eval_seq(f₂,s) is true, return f which is true.
  • if eval_seq(f₁,s) is false or eval_seq(f₂,s) is false, return f which is false.
  • otherwise return f which is pending.
• case f is f₁ OR f₂
  • if eval_seq(f₁,s) is true or eval_seq(f₂,s) is true, return f which is true.
  • if eval_seq(f₁,s) is false and eval_seq(f₂,s) is false, return f which is false.
  • otherwise return f which is pending.
• case f is NOT f'
  • if eval_seq(f') is true return f which is false.
  • if eval_seq(f') is false return f which is true.
  • otherwise return f which is pending.
• case f which is atomic (a SEFL program p)
  • construct complement(p) and execute it in the current state. If there exist successful paths, f is false, otherwise it is true.

complement(p:Program) : Program

• case p = {q₁ ; q₂ ; ... ; q_m}
  • return {complement(q₁) || complement(q₂) || ... || complement(q_m)}
• case p = Constrain(v,e) return Constrain(v,complement(e))