Changeset 2224 for src

Timestamp:

Jul 20, 2012, 4:29:31 PM (9 years ago)

Author:

campbell

Message:

Proper whole program result in RTLabs/Traces

File:

• src/RTLabs/Traces.ma (modified) (2 diffs)

src/RTLabs/Traces.ma

@@ -1919 +1919 @@
 ] qed.
 
-(*
+lemma init_state_is : ∀p,s.
+  make_initial_state p = OK ? s →
+  𝚺b. match s with [ Callstate fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
+   | _ ⇒ False ].
+#p #s
+@bind_ok #m #Em
+@bind_ok #b #Eb
+@bind_ok #f #Ef
+#E whd in E:(??%%); destruct
+%{b} whd
+% // @Ef
+qed.
+
+definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_state (make_global p) ≝
+λp,s,I. mk_RTLabs_state (make_global p) s [init_state_is p s I] ?.
+cases (init_state_is p s I) #b
+cases s
+[ #f #fs #m *
+| #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
+| #rv #rr #fs #m *
+| #r *
+] qed.
+
 theorem program_trace_exists :
   termination_oracle →
@@ -1929 +1951 @@
   
   ∀NOIO:exec_no_io … plain_trace.
+  ∀NW:not_wrong … plain_trace.
   
-  let flat_trace ≝ make_whole_flat_trace p s NOIO I in
+  let flat_trace ≝ make_whole_flat_trace p s NOIO NW I in
   
-  trace_whole_program_exists (RTLabs_status (make_global p)) s.
+  trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I).
+
 #ORACLE #p #s #I
 letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
-#NOIO
-letin flat_trace ≝ (make_whole_flat_trace p s NOIO I)
-whd
-@(whole_structured_trace_exists … flat_trace)
-//
-[ whd
-*)
+#NOIO #NW
+letin flat_trace ≝ (make_whole_flat_trace p s NOIO NW I)
+whd 
+@(whole_structured_trace_exists (make_global p) p ? ORACLE)
+[ 3: @flat_trace | 4: @I
+| *: cases daemon
+] qed.
+
 
 lemma simplify_exec : ∀ge.∀s,s':RTLabs_state ge.