Revive thermostat visualization.

bnat.v

@@ -4,6 +4,12 @@ Inductive bnat: nat -> Set :=
   | bO n: bnat (S n)
   | bS n: bnat n -> bnat (S n).
 
+Fixpoint to_nat n (b: bnat n): nat :=
+  match b with
+  | bO _ => 0
+  | bS _ x => S (to_nat x)
+  end.
+
 Section alt_rect.
 
   Variables

Types.hs → examples/thermostat/visualization/Types.hs

@@ -4,14 +4,9 @@ data Location =
   Up | Right | Down | Left | -- rotator locations
   Heat | Cool | Check -- thermostat locations
   deriving Eq
-data Range =
-  I01 | I12 | I23 | I34 | I45 | -- bounded rotator intervals
-  OI_1 | OI12 | OI23 | OI34 | OI4_ | -- unbounded rotator intervals
-  CI0_C | CIC_12 | CI12_1 | CI1_2 | CI2_3 | CI3_ | -- thermostat clock intervals
-  TI_5 | TI5_6 | TI6_8 | TI8_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)
+data Vertex = Vertex Kind Location Integer Integer deriving (Show, Eq)
 
 instance Show Kind where show Cont = "C"; show Disc = "D"
 instance Show Location where

examples/thermostat/visualization/generate_transitions.sh

@@ -4,6 +4,6 @@ echo "module GeneratedTransitions where"
 echo "import Types"
 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 "edges = map (\(a, (b, c, d), (e, (f, g, h))) -> (Vertex (if a then Cont else Disc) b c d, Vertex (if e then Cont else Disc) f g h)) raw_edges"
 echo "raw_edges"
 coqc -R /data/home/eelis/soft/CoRN CoRN generate_transitions.v | head -n 1

examples/thermostat/visualization/generate_transitions.v

@@ -1,26 +1,11 @@
-Require Import thermostat.
 Require abstract_as_graph.
-Require Import CRln.
-
-Let conc_sys := concrete_system.
-Let region: Set := abstract.Region abs_sys.
-
-Require abstract.
-
-Let abs_state: Set := @abstract.State conc_sys (abstract.Region abs_sys).
-
-Definition initstate: abs_state
-  := (thermostat.Heat, (thermostat.CI0_C, thermostat.TI6_8)).
-
-Definition all_transitions: list (abs_state * abs_state) :=
-  flat_map (fun s: abs_state =>
-    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)).
+Require Import CRln c_util.
+Require Import thermostat.abs.
+Require Import thermostat.conc.
 
+Let abs_sys := abs.system milli.
 Let graph := abstract_as_graph.g abs_sys.
-
-Let init := (abstract_as_graph.Cont, initstate).
+Let init: digraph.Vertex graph := (true, (conc.Heat, (bnat.bO _, bnat.bO _))).
 
 Lemma NoDup_one X (x: X): NoDup (x :: nil). auto. Qed.
 
@@ -29,15 +14,25 @@ Definition reachables: list (digraph.Vertex graph) :=
 
 Definition exported_edges: list (digraph.Vertex graph * digraph.Vertex graph)
   := flat_map (fun v => map (pair v) (digraph.edges v)) reachables.
-  (* := digraph.flat_edge_list graph. *)
+
+Definition PrintedVertex := (bool * (Location * nat * nat))%type.
+
+Definition printVertex (v: digraph.Vertex graph): PrintedVertex :=
+  (fst v, (fst (snd v), (bnat.to_nat (fst (snd (snd v)))), bnat.to_nat (snd (snd (snd v))))).
+
+Definition printed_edges: list (PrintedVertex * PrintedVertex)
+  := map (fun e => (printVertex (fst e), printVertex (snd e))) exported_edges.
 
 Infix ":" := cons (at level 60, right associativity) : list_scope.
 Notation "[]" := nil.
+Notation True := true.
+Notation False := false.
+  (* so that it's valid Haskell *)
 
 Set Printing Depth 10000.
 Set Printing Width 1000000.
 
 Require Import abstract_as_graph.
   (* so that names aren't qualified in the output *)
 
-Eval vm_compute in exported_edges.
+Eval vm_compute in printed_edges.

graph_to_dot.hs → examples/thermostat/visualization/graph_to_dot.hs

@@ -3,13 +3,6 @@ import Types
 import List (nub)
 import Prelude hiding (Left, Right)
 
-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_C -> 0; CIC_12 -> 0.1; CI12_1 -> 0.5; CI1_2 -> 1; CI2_3 -> 2; CI3_ -> 3
-  TI_5 -> 0; TI5_6 -> 5; TI6_8 -> 6; TI8_9 -> 8; TI9_10 -> 9; TI10_ -> 10
-
 location_index :: Location -> Int
 location_index l = case l of
   Up -> 0; Right -> 1; Down -> 2; Left -> 3
@@ -18,18 +11,18 @@ location_index l = case l of
 kind_index :: Kind -> Int
 kind_index Cont = 0; kind_index Disc = 1
 
-ranges_adjacent :: Range -> Range -> Bool
-ranges_adjacent r r' = abs (range_coordinate r - range_coordinate r') <= 1
+-- ranges_adjacent :: Range -> Range -> Bool
+-- ranges_adjacent r r' = abs (range_coordinate r - range_coordinate r') <= 1
 
-vertices_adjacent :: Vertex -> Vertex -> Bool
-vertices_adjacent (Vertex _ _ a a') (Vertex _ _ b b') =
-  ranges_adjacent a b && ranges_adjacent a' b'
+-- vertices_adjacent :: Vertex -> Vertex -> Bool
+-- vertices_adjacent (Vertex _ _ a a') (Vertex _ _ b b') =
+--   ranges_adjacent a b && ranges_adjacent a' 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 * 600 + fromIntegral (kind_index k * 90)) ++ "," ++
-  show (100 + range_coordinate r' * 200 + fromIntegral (kind_index k * 15) + fromIntegral (location_index l * 30)) ++ "\"]\n"
+  show (100 + r * 600 + fromIntegral (kind_index k * 90)) ++ "," ++
+  show (100 + r' * 200 + fromIntegral (kind_index k * 15) + fromIntegral (location_index l * 30)) ++ "\"]\n"
 
 edge_visible :: Vertex -> Vertex -> Bool
 edge_visible v@(Vertex k l r r') v'@(Vertex k' l' u u') =

examples/thermostat/visualization/show_graph.sh

@@ -1,5 +1,4 @@
 #!/bin/sh
 set -e
-scons -j 2 thermostat.vo
 ./generate_transitions.sh > GeneratedTransitions.hs
 runhaskell graph_to_dot.hs | neato -n -Elen=5 -Tpng > t.png