(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Robot
imports
  ClockView
  SPRViewSingle
  "HOL-Library.Saturated"
begin

(*>*)
subsection‹The Robot›

text‹
 label{sec:kbps-theory-robot}

 begin{figure}[tb]
 \includegraphics[width=\textwidth]{robot_clock}
 \caption{The implementation of the robot using the clock semantics.}
 \label{fig:kbps-theory-robot-clock}
 end{figure}

 begin{figure}[tb]
 \includegraphics[width=\textwidth]{robot_spr}
 \caption{The implementation of the robot using the SPR semantics.}
 \label{fig:kbps-theory-robot-spr}
 end{figure}

  the autonomous robot of \S\ref{sec:kbps-robot-intro}: we are
  for an implementation of the KBP:
 begin{center}
 \begin{tabular}{lll}
 $\mathbf{do}$\\
 & $\gcalt$ $\mathbf{K}_{\mbox{robot}}$ \textsf{goal} & $pan style='color:turquoise'>\rightarrow$ \textsf{Halt}\\
 & $\gcalt$ $\lnot\mathbf{K}_{\mbox{robot}}$ \textsf{goal} & $\rightarrow$ \textsf{Nothing}\\
 $\mathbf{od}$\\
 \end{tabular}
 end{center}
  an environment where positions are identified with the natural
 , the robot's sensor is within one of the position, and the
  \textsf{goal} is true when the position is in
 \{2,3,4\}$. The robot is initially at position zero, and the effect
  its \textsf{Halt} action is to cause the robot to instantaneously
  at its current position. A later \textsf{Nothing}
  may allow the environment to move the robot further to the
 .

  obtain a finite environment, we truncate the number line at 5,
  is intuitively sound for determinining the robot's behaviour due
  the synchronous view, and the fact that if it reaches this
  position then it can never satisfy its objective. Running
  Haskell code generated by Isabelle yields the automata shown in
 ~\ref{fig:kbps-theory-robot-clock} and
 ~\ref{fig:kbps-theory-robot-spr} for the clock and synchronous
  recall semantics respectively. These have been minimised using
 's algorithm 🚫‹"DBLP:journals/acta/Gries73"›.

  (inessential) labels on the states are an upper bound on the set
  positions that the robot considers possible when it is in that
 . Transitions are annotated with the observations yielded by the
 . Double-circled states are those in which the robot performs
  \textsf{Halt} action, the others \textsf{Nothing}. We observe that
  synchronous perfect-recall view yields a ``ratchet'' protocol,
 .e. if the robot learns that it is in the goal region then it halts
  all time, and that it never overshoots the goal region. Conversely
  clock semantics allows the robot to infinitely alternate its
  depending on the sensor reading. This is effectively the
  of the intuitive implementation that halts iff the sensor
  three or more.

  can also see that minimisation does not yield the smallest automata
  could hope for; in particular there are a lot of redundant states
  the prescribed behaviour is the same but the robot's state of
  different. This is because our implementations do not
  what happens on invalid observations, which we have modelled
  errors instead of don't-cares, and these extraneous distinctions
  preserved by bisimulation reduction. We discuss this further in
 S\ref{sec:kbps-alg-auto-min}.

\<close>(*<*)

(*

The environment protocol does nothing if the robot has signalled halt,
or chooses a new position and sensor reading if it hasn't.

We need a finite type to represent positions and observations. It is
sufficient to go to 5, for by then we are either halted in the goal
region or have gone past it.

*)

type_synonym digit = "5 sat"

datatype Agent = Robot
datatype EnvAct = Stay | MoveRight
datatype ObsError = Left | On | Right
datatype Proposition = Halted | InGoal
datatype RobotAct = NOP | Halt

type_synonym Halted = bool
type_synonym Pos = digit
type_synonym Obs = digit
type_synonym EnvState = "Pos × Obs × Halted"

definition
  envInit :: "EnvState list"
where
  "envInit ≡ [(0, 0, False), (0, 1, False)]"

definition
  envAction :: "EnvState → (EnvAct × ObsError) list"
where
  "envAction ≡ λ_. [ (x, y) . x ← [Stay, MoveRight], y ← [Left, On, Right] ]"

definition
  newObs :: "digit → ObsError → digit"
where
  "newObs pos obserr ≡
              case obserr of Left → pos - 1 | On → pos | Right → pos + 1"

definition
  envTrans :: "EnvAct × ObsError → (Agent → RobotAct) → EnvState → EnvState"
where
  "envTrans ≡ λ(move, obserr) aact (pos, obs, halted).
    if halted
      then (pos, newObs pos obserr, halted)
      else
        case aact Robot of
           NOP → (case move of
                      Stay → (pos, newObs pos obserr, False)
                    | MoveRight → (pos + 1, newObs (pos + 1) obserr, False))
         | Halt → (pos, newObs pos obserr, True)"


definition
  envObs :: "EnvState → Obs"
where
  "envObs ≡ λ(pos, obs, halted). obs"

definition
  envVal :: "EnvState → Proposition → bool"
where
  "envVal ≡ λ(pos, obs, halted) p.
     case p of Halted → halted
             | InGoal → 2 ≤ pos ∧ pos ≤ (4 :: 5 sat)"

(* The KBP, clearly subjective. *)

definition
  kbp :: "(Agent, Proposition, RobotAct) KBP"
where
  "kbp ≡ [ ( guard = K (Kprop InGoal), action = Halt ),
           ( guard = Knot (K (Kprop InGoal)), action = NOP ) ]"

(*<*)

lemma Agent_univ: "(UNIV :: Agent set) = {Robot}"
  unfolding UNIV_def
  apply auto
  apply (case_tac x)
  apply auto
  done

instance Agent :: finite
  apply intro_classes
  apply (auto iff: Agent_univ)
  done

instantiation Agent :: linorder
begin

definition
  less_Agent_def: "(x::Agent) < y ≡ False"

definition
  less_eq_Agent_def: "(x::Agent) ≤ y ≡ x = y"

instance
  apply intro_classes
  unfolding less_Agent_def less_eq_Agent_def
  apply simp_all
  apply (case_tac x)
  apply (case_tac y)
  apply simp
  done
end

(*>*)

subsubsection‹Locale instantiations›

interpretation Robot:
  Environment "λ_. kbp" envInit envAction envTrans envVal "λ_. envObs"
  apply unfold_locales
  apply (auto simp: kbp_def)
  apply ((case_tac a, simp)+)
  done

subsubsection‹The Clock view implementation›

interpretation Robot_Clock:
  FiniteLinorderEnvironment "λ_. kbp" envInit envAction envTrans envVal "λ_. envObs" "fromList [Robot]"
  apply unfold_locales
  apply (simp add: Agent_univ)
  done

abbreviation "Agents ≡ ODList.fromList [Robot]"

definition
  robot_ClockDFS :: "((EnvState, RobotAct list) clock_acts_trie, (EnvState, digit) clock_trans_trie) AlgState"
where
  "robot_ClockDFS ≡ ClockAutoDFS Agents (λ_. kbp) envInit envAction envTrans envVal (λ_. envObs) Robot"

definition
  robot_ClockAlg :: "Agent → (digit, RobotAct, EnvState odlist × EnvState odlist) Protocol"
where
  "robot_ClockAlg ≡ mkClockAuto Agents (λ_. kbp) envInit envAction envTrans envVal (λ_. envObs)"

lemma (in FiniteLinorderEnvironment)
  "Robot.Clock.implements robot_ClockAlg"
  unfolding robot_ClockAlg_def by (rule Robot_Clock.mkClockAuto_implements)

subsubsection‹The SPR view implementation›

interpretation Robot_SPR:
  FiniteSingleAgentEnvironment "λ_. kbp" envInit envAction envTrans envVal "λ_. envObs" "Robot"
  apply unfold_locales
  apply (case_tac a, simp)
  done

definition
  robot_SPRSingleDFS :: "(RobotAct, digit, EnvState) SPRSingleAutoDFS"
where
  "robot_SPRSingleDFS ≡ SPRSingleAutoDFS kbp envInit envAction envTrans envVal (λ_. envObs) Robot"

definition
  robot_SPRSingleAlg :: "Agent → (digit, RobotAct, EnvState odlist) Protocol"
where
  "robot_SPRSingleAlg ≡ mkSPRSingleAuto kbp envInit envAction envTrans envVal (λ_. envObs)"

lemma (in FiniteSingleAgentEnvironment)
  "Robot.Robot.SPR.implements robot_SPRSingleAlg"
  unfolding robot_SPRSingleAlg_def by (rule Robot.Robot_SPR.mkSPRSingleAuto_implements)

end
(*>*)