如何在COQ中使用持久状态建模？

Question

在我们的大学任务中，我们被要求在谓词和命题逻辑中对我们选择的对象进行建模。我的小组参加了555个计时器集成电路。目前，我们面临着建模该对象的行为的问题，该对象（尤其是SR-LATCH部分）。

这个问题似乎源于以下事实：SR-Latch使用组合逻辑无法描述。

我们不确定手头的任务是否可能发生，并且希望获得一些建议，以及在这种情况下使用的技术是否可能。

到目前为止，我们的描述就像是这样：

Require Import BenB.

(* time elapsed from some point in past in microseconds as real numbers *)
Definition T := R.

(* durations in microseconds as real numbers *)
Definition D := R.

(* some arbitrary constant duration time-delta representing the oscialltion period / 2 *)
Variable td: D.

(* a type representing the io pins of the 555 IC *)
Inductive Pin: Type :=
    | output : Pin
    | voltage : Pin
    | trigger : Pin
    | threshold : Pin
    | reset : Pin
    | ground : Pin
    | control : Pin
    | discharge : Pin
.
(* predicate representing the logical state of the pin at certain time *)
Variable isHigh : T -> Pin -> Prop.


(* represents the if the current can flow through the 555 IC *)
Definition ICPowered (t:T) :=
    (isHigh t voltage)
    /\
    ~(isHigh t ground)
.

Definition srLatch (t: T) := 
    (isHigh t reset) 
    /\
    
.

Definition initialConditions := 
   ICPowered
.

(* Definition describing the expected oscillating behaviour of the output signal *)
Definition oscillationObligation :=
forall t: T,
    ((isHigh t output) -> ~(isHigh (t+d) output))
    /\
    (~(isHigh t output) -> (isHigh (t+d) output))
.


Definition correctnessTheorem := 
    initialConditions -> oscillationObligation
.

PS我们假设我们可以使用论坛作为学习资源，毫无疑问，将提及工作中使用的所有来源，包括我们可能会夺回的任何答案。