Require Import BenB.
Require Import BenB2.

(* ====================================================================== *)

(*
   Title:
   ======
   Authors:
   [
   Daniel Anthes s...,
   Sean Gies s...,
   Eddie the Eagle s..,
   Nick Stracke s4771192
   ]
*)

(* ====================================================================== *)

(*
   [
     This file has to be a valid script, meaning that it
     can be executed by Coq.
     Therefore, explanations in natural language have to be between
     comment markers.

     In this project template, text within square brackets (within
     comment markers) is intended to clarify what needs to be
     written where.

     In the final version, we expect that all these blocks have been
     replaced by (your) proper content.
   ]

*)

(*
   Abstract:
   =========
   [
     For the intermediate version of this project:
     Explain briefly which perspective of which artifact will be
     studied and why this topic has been chosen.
   ]

   [
     And for the final version of this project:
     Explain whether you managed to prove the correctness theorem.
     And how did that go: did you have to change a lot compared to
     the intermediate version, or could you use your formalization
     without many modifications?
   ]

*)

(*
   Focus:

   Modeling Goal:
   ==============
   [ Verification model / Demonstration model / Construction model ]


   Fragment of reality:
   ====================
   [ ... ]


   Perspective:
   ============
   [ ... ]

*)


(*
   Abstractions or simplifications:
   ================================
   [
     Depending on the chosen focus, you may simplify certain aspects of
     your artifact.
     If you are modeling some kind of home automation system, it is not
     unreasonable to assume that the net power is constant, although this
     is not exactly the case in reality. However, if you are modeling an
     artifact that protects against high peaks of power, these fluctuations
     should be part of the model.

     Write down explicitly which assumptions you have made to simplify
     the artifact.
   ]

*)

(* ====================================================================== *)

(* Domain model *)

(* Domains (including their meaning) *)

Definition T := R.
(* Time *)

Variable B : Set.
(* Buttons of the equalizer *)

Definition D := R.
(* Durations of songs *)


(* Constants (including their meaning) *)


(* Functions (including their meaning) *)

(* Predicates (including their meaning and measurements) *)

Variable vinyl_on (* t *)  : T -> Prop.
(* vinyl is on the platter at time t *)
(* look at the turn table *)

Variable move_arm_in_position (* t *) : T -> Prop.
(* move arm over the platter at time t *)
(* look if the arm starts moving at time t *)


Variable power_in : Prop.
(* A voltage of 230V is being supplied to the powerstrip *)
(* Use a multimeter to measure the voltage *)

Variable eq_button_pushed (* b *) : B -> T -> Prop.
(* button b of the equalizer is pushed in *)
(* look if button b is pushed in *)

Variable ls_out_eq (* t *) : T -> Prop.
(* There is an equalized audio signal coming out of the left speaker *)
(* Listen if there is an audio signal *)

Variable ls_out_uneq (* t *) : T -> Prop.
(* There is an unequalized audio signal coming out of the left speaker *)
(* Listen if there is an audio signal *)

Variable rs_out_eq (* t *) : T -> Prop.
(* There is an equalized audio signal coming out of the right speaker *)
(* Listen if there is an audio signal *)

Variable rs_out_uneq (* t *) : T -> Prop.
(* There is an unequalized audio signal coming out of the right speaker *)
(* Listen if there is an audio signal *)

Variable sub_out_eq (* t *) : T -> Prop.
(* There is an equalized audio signal coming out of the subwoofer *)
(* Listen if there is an audio signal *)

Variable sub_out_uneq (* t *) : T -> Prop.
(* There is an unequalized audio signal coming out of the subwoofer *)
(* Listen if there is an audio signal *)

Variable is_on (* t *) : T -> Prop.
(* The on button of the amplifier is pushed *)
(* Check if the button is pressed *)

Variable line_level (* t *) : T -> Prop.
(* Low level signal *)
(* Measure if there is an output *)

Variable lost_heat (* t *) : T -> Prop.
(* Heat leaving the amplifier *)
(* Feel if there is hot air leaving the amplifier *)

Variable line_level_high_eq :T -> Prop.
(* equalized, boosted signal for the speaker *)
(* check output *)

Variable line_level_high_uneq :T -> Prop.
(* unequalized, boosted signal for the speaker *)
(* check output *)

Variable line_level_loq_eq :T -> Prop.
(* equalized, boosted signal for the subwoofer *)
(* check output *)

Variable line_level_hloq_uneq :T -> Prop.
(* unequalized, boosted signal for the subwoofer *)
(* check output *)

Variable amp_power

(* ====================================================================== *)

(* Auxiliary predicates (including their meaning) *)

(*
   [
     At this place within this template you may define as many
     auxiliary predicates as you want, but do not forget to include
     their meaning.
   ]
*)

(* ====================================================================== *)

(* Components *)

(*
   [
     For each component you have to specify the following information:

     OUTSIDE comment markers:
     - The 'Definition' to be read by Coq, in a readable layout that
       matches the mathematical structure of the formula.

     WITHIN comment markers:
     - The specification of the component in natural language. Obviously,
       this specification should be consistent with the formula used
       by Coq.
     - If appropriate, a short explanation in natural language about
       the choices that have been made.
   ]
*)

Definition Record_Player :=

.

Definition Pre_Amp :=

.

Definition Amp :=

.

Definition Left_Speaker :=

.

Definition Right_Speaker :=

.

Definition Subwoofer :=

.



(* ====================================================================== *)

(* Specification of the overall system *)

(*
   [
     Here you have to specify:

     OUTSIDE comment markers:
     - The 'Definition' to be read by Coq, in a readable layout that
       matches the mathematical structure of the formula.

     WITHIN comment markers:
     - The specification of the overall system in natural language.
       Obviously, this specification should be consistent with the
       formula used by Coq.
     - If appropriate, a short explanation in natural language about
       the choices that have been made.
   ]
*)

Definition Hifi_soundsystem_with_record_player :=
forall t:T,
            vinyl_on t
        /\
            move_arm_in_position (t+1)
        /\
            power_in
        /\
            is_on (t+2)
    ->
            (
                (
                exists b:B,
                    eq_button_pushed b (t+2)
                )
            ->
                ls_out_eq (t+2) /\ rs_out_eq (t+2) /\ sub_out_eq (t+2)
            )
        /\
            (
                (
                ~ exists b:B,
                    eq_button_pushed b (t+2)
                )
            ->
                ls_out_uneq (t+2) /\ rs_out_uneq (t+2) /\ sub_out_uneq (t+2)
            )
.
(* ====================================================================== *)

(* Extras *)

(*
   [
     It is very likely that you do not need any extras!

     However, if it turns out during your proof that you have to prove
     several times (almost) the same, then you may define a 'Lemma' at
     this place, followed by its proof. And in the proof of the correctness
     theorem, you may apply this lemma several times.
     Note that it is always allowed to add lemmas to this script!

     Sometimes it happens that Coq has troubles with 'trivial' properties
     of numbers, that cannot be solve easily using 'lin_solve'.
     In such situations, you may contact your supervisor and discuss
     whether this may be solved by adding an 'Axiom', which can also be
     applied later on within the proof of the correctness theorem.
   ]
*)

(* Correctness theorem *)

(* ====================================================================== *)

(*
   [
     Write down your correctness theorem in the usual notation:
     Theorem CorTheorem:
     Component1 /\ Component2 /\ ... /\ ComponentN -> SpecOfTheOverallSystem.

     Note that for the intermediate version, you should keep this
     theorem within comment markers, otherwise you will get a red cross
     for stating a theorem without a proof.

     For the final version you obviously have to remove these comment
     markers and probide a real proof!
   ]
*)

(*
Theorem CorTheorem:
    Record_Player /\ Pre_Amp /\ Amp /\ Left_Speaker /\ Right_Speaker /\ Subwoofer /\ Powerstrip
->
    Hifi_soundsystem_with_record_player
.
*)