Make thermostat more closely resemble Alur's. Use Program to make som…

…e things nicer.

Ignore-this: a222319b0347a3e215f0b5b5a0aed9

darcs-hash:20090423214845-bab43-1ae9978ebd297455ee782e5a19caefa1f614910c.gz

Types.hs

@@ -5,10 +5,10 @@ data Location =
   Heat | Cool | Check -- thermostat locations
   deriving Eq
 data Range =
-  I01 | I12 | I23 | I34 | I45 |
-  OI_1 | OI12 | OI23 | OI34 | OI4_ |
-  CI0_12 | CI_12 | CI12_1 | CI1_2 | CI2_3 | CI3_ | -- thermostat clock intervals
-  TIC_3 | TI3_45 | TI45_5 | TI5_6 | TI6_9 | TI9_10 | TI10_ -- thermostat temperature intervals
+  I01 | I12 | I23 | I34 | I45 | -- bounded rotator intervals
+  OI_1 | OI12 | OI23 | OI34 | OI4_ | -- unbounded rotator intervals
+  CI0_D | CID_12 | CI12_1 | CI1_2 | CI2_3 | CI3_ | -- thermostat clock intervals
+  TIC_45 | TI45_5 | TI5_6 | TI6_9 | TI9_10 | TI10_ -- thermostat temperature intervals
   deriving (Show, Eq)
 data Kind = Cont | Disc deriving Eq
 data Vertex = Vertex Kind Location Range Range deriving (Show, Eq)

c_util.v

@@ -735,8 +735,6 @@ Qed.
 Lemma CRnonNeg_nonPos_mult_inv: forall x (p: CRnonNeg x) y,
   CRnonPos (x * y) -> CRnonPos y.
 Proof with auto.
-  unfold CRnonNeg, CRnonPos.
-  intros.
 Admitted.
 
 Axiom CR_lt_eq_dec: forall (x y: CR), sum (x==y) (sum (x<y) (y<x)).

clean.sh

@@ -0,0 +1,2 @@
+#!/bin/sh
+rm -f *.vo *.glob

flow.v

@@ -162,7 +162,7 @@ End scale.
 Module positive_linear.
 Section contents.
 
-  Variable r: positive. (* todo: generalize to Qpos, CRpos *)
+  Variable r: Qpos.
 
   Definition raw (x: CR) (t: Time): CR := x + 'r * t.
 
@@ -190,23 +190,27 @@ Section contents.
 
   Definition f: Flow CRasCSetoid := Build_Flow morphism A B.
 
-  Definition inv (x x': CR): Time := '(1#r) * (x' - x).
+  Definition inv (x x': CR): Time := '(Qinv r) * (x' - x).
 
   Lemma inv_correct x x': f x (inv x x') == x'.
+  Proof with auto.
     intros.
     unfold f, inv. simpl bsm. unfold raw.
     rewrite (Rmul_assoc CR_ring_theory).
     rewrite CRmult_Qmult.
-    rewrite Qmult_inv.
+    rewrite Qmult_inv_r.
       rewrite (Rmul_1_l CR_ring_theory).
       symmetry. apply t11.
-    reflexivity.
+    intro.
+    symmetry in H.
+    apply (Qlt_not_eq 0 r)...
+    apply Qpos_prf.
   Qed.
 
   Lemma increasing: forall x : CRasCSetoid, strongly_increasing (f x).
     repeat intro. simpl. unfold raw. apply t1_rev. 
     apply CRmult_lt_pos_r. assumption.
-    apply positive_CRpos.
+    apply Qpos_CRpos.
   Qed.
 
   Definition mono: mono f := inl increasing.

generate_transitions.sh

@@ -6,4 +6,4 @@ echo "import Prelude hiding (Either(..))"
 echo "edges :: [(Vertex, Vertex)]"
 echo "edges = map (\(a, (b, (c, d)), (e, (f, (g, h)))) -> (Vertex a b c d, Vertex e f g h)) raw_edges"
 echo "raw_edges"
-/home/gi/cek/trunk/bin/coqc -R /home/gi/cek/CoRN CoRN generate_transitions.v | head -n 1
+coqc -R /data/home/eelis/soft/CoRN CoRN generate_transitions.v | head -n 1

generate_transitions.v

@@ -5,20 +5,20 @@ Require Import CRln.
 Let conc_sys := concrete_system.
 Let abs_sys := abstract_system (1#100).
 
-Let region: Set := c_abstract.Region abs_sys.
+Let region: Set := abstract.Region abs_sys.
 
-Require c_abstract.
+Require abstract.
 
-Let abs_state: Set := @c_abstract.State conc_sys (c_abstract.Region abs_sys).
+Let abs_state: Set := @abstract.State conc_sys (abstract.Region abs_sys).
 
 Definition initstate: abs_state
-  := (thermostat.Heat, (thermostat.CI0_12, thermostat.TI6_9)).
+  := (thermostat.Heat, (thermostat.CI0_D, thermostat.TI6_9)).
 
 Definition all_transitions: list (abs_state * abs_state) :=
   flat_map (fun s: abs_state =>
-    map (pair s) (map (pair (fst s)) (c_abstract.cont_trans conc_sys s) ++ 
-    c_abstract.disc_trans conc_sys s))
-   (@c_abstract.states conc_sys _ _ (c_abstract.regions abs_sys)).
+    map (pair s) (map (pair (fst s)) (abstract.cont_trans conc_sys s) ++
+    abstract.disc_trans conc_sys s))
+   (@abstract.states conc_sys _ _ (abstract.regions abs_sys)).
 
 Let graph := abstract_as_graph.g abs_sys.
 

geometry.v

@@ -6,9 +6,11 @@ Require Export dec_overestimator.
 Set Implicit Arguments.
 Open Local Scope CR_scope.
 
-Definition Range: Type := { r: CR * CR | fst r <= snd r }.
+Definition Range: Type := sig (fun r: CR * CR => fst r <= snd r).
 
-Definition unit_range (c: CR): Range := existT _ (c, c) (CRle_refl c).
+Hint Immediate CRle_refl.
+
+Program Definition unit_range (c: CR): Range := (c, c).
 
 Section option_setoid.
 
@@ -67,15 +69,14 @@ Definition CRmin_of_upper_bounds (a b: option CR): option CR :=
   | Some a, Some b => Some (CRmin a b)
   end.
 
-
 Definition OpenRange: Type := sig OCRle.
 
 Coercion open_range (r: Range): OpenRange :=
   match r with
-  | existT (x, y) H => existT _ (Some x, Some y) H
+  | exist (x, y) H => exist _ (Some x, Some y) H
   end.
 
-Definition unbounded_range: OpenRange := existT _ (None, None) I.
+Program Definition unbounded_range: OpenRange := (None, None).
 
 Definition range_left (r: Range): CR := fst (proj1_sig r).
 Definition range_right (r: Range): CR := snd (proj1_sig r).
@@ -345,24 +346,15 @@ Proof.
   split; eapply oranges_share_point; eauto.
 Qed.
 
-Definition map_range (f: CR -> CR) (fi: increasing f) (r: Range): Range.
-  intros.
-  exists (f (fst (proj1_sig r)), f (snd (proj1_sig r))).
-  simpl.
-  apply fi.
-  destruct r.
-  assumption.
-Defined. (* for some reason Program Definition won't work here.. *)
-  (* i think it must be because CR is in Type *)
+Program Definition map_range (f: CR -> CR) (fi: increasing f) (r: Range): Range :=
+  (f (fst (proj1_sig r)), f (snd (proj1_sig r))).
 
-Definition map_orange (f: CR -> CR)
-  (fi: increasing f) (r: OpenRange): OpenRange.
-Proof with simpl; auto.
-  intros.
-  exists (option_map f (fst (`r)), option_map f (snd (`r))).
-  destruct r. destruct x.
-  destruct s... destruct s0...
-Defined.
+Next Obligation. destruct r. apply fi. assumption. Qed.
+
+Program Definition map_orange (f: CR -> CR) (fi: increasing f) (r: OpenRange): OpenRange
+  := (option_map f (fst (`r)), option_map f (snd (`r))).
+
+Next Obligation. destruct r as [[[a|] [b|]] m]; simpl; auto. Qed.
 
 Definition in_map_range p r (f: CR -> CR) (i: increasing f): in_range r p ->
   in_range (map_range i r) (f p).
@@ -385,15 +377,11 @@ Section scaling.
 
   Variables (s: CR) (H: '0 <= s).
 
+  Hint Resolve CRle_mult.
+
   Program Definition scale_orange (r: OpenRange): OpenRange :=
     (option_map (CRmult s) (fst (`r)), option_map (CRmult s) (snd (`r))) .
-  Next Obligation. Proof with auto.
-    destruct r as [[a b] h].
-    destruct a... destruct b...
-    simpl in *. apply CRle_mult...
-  Qed.
-
-Hint Resolve CRle_mult.
+  Next Obligation. destruct r as [[[a|] [b|]] h]; simpl; auto. Qed.
 
   Lemma in_scale_orange p r : in_orange r p ->
     in_orange (scale_orange r) (s * p).

graph_to_dot.hs

@@ -7,8 +7,8 @@ range_coordinate :: Range -> Double
 range_coordinate r = case r of
   I01 -> 0; I12 -> 1; I23 -> 2; I34 -> 3; I45 -> 4
   OI_1 -> 0; OI12 -> 1; OI23 -> 2; OI34 -> 3; OI4_ -> 4
-  CI0_12 -> 0; CI_12 -> 0; CI12_1 -> 0.5; CI1_2 -> 1; CI2_3 -> 2; CI3_ -> 3
-  TIC_3 -> 0; TI3_45 -> 3; TI45_5 -> 4.5; TI5_6 -> 5; TI6_9 -> 6; TI9_10 -> 9; TI10_ -> 10
+  CI0_D -> 0; CID_12 -> 0.1; CI12_1 -> 0.5; CI1_2 -> 1; CI2_3 -> 2; CI3_ -> 3
+  TIC_45 -> 0; TI45_5 -> 4.5; TI5_6 -> 5; TI6_9 -> 6; TI9_10 -> 9; TI10_ -> 10
 
 location_index :: Location -> Int
 location_index l = case l of
@@ -28,7 +28,7 @@ vertices_adjacent (Vertex _ _ a a') (Vertex _ _ b b') =
 pos_label :: Vertex -> String
 pos_label (Vertex k l r r') = "[label=\"" ++ show l ++ "\",color=" ++
   (if k == Cont then "red" else "blue") ++ ",pos=\"" ++
-  show (100 + range_coordinate r * 400 + fromIntegral (kind_index k * 90)) ++ "," ++
+  show (100 + range_coordinate r * 600 + fromIntegral (kind_index k * 90)) ++ "," ++
   show (100 + range_coordinate r' * 200 + fromIntegral (kind_index k * 15) + fromIntegral (location_index l * 30)) ++ "\"]\n"
 
 edge_visible :: Vertex -> Vertex -> Bool