source: src/RTLabs/RTLabsExecToTrace.ma @ 3096

Last change on this file since 3096 was 3096, checked in by tranquil, 7 years ago

preliminary work on closing correctness.ma

File size: 1.4 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "RTLabs/MeasurableToStructured.ma".
16include "common/StatusSimulation.ma".
17
18axiom produce_rtlabs_flat_trace :
19  ∀p : RTLabs_program.∀n : ℕ.∀st,tr.
20    exec_steps_with_obs RTLabs_ext_pcs p n = return 〈st, tr〉 →
21  ∃st_init.make_ext_initial_state … p = return st_init ∧
22  ∃ft : flat_trace (RTLabs_status (make_global p)) st_init st.
23  ft_observables … ft = tr.
Note: See TracBrowser for help on using the repository browser.