Hello everyone. I am trying to model a real-time distributed system in
HOL4. Please check the implementations and suggest any
improvement/correction please.
*Equations: *
L3 *t* = w1 * L1 *t* + w2 * L2 *t*
L5 *t* = L3 *t* - a * (L4 *t* - b)
where w1,w2 & a are constants.
L represents the lists (one element for each node of distributed system)
*t* represents the time
i.e. L5 t means List 5 at time t
I need to use L5 in the algorithm, L3 is not used elsewhere in the algo.
To model time, I model the lists as num->(real list) where for each time t
(num), a list is represented with the length equal to the number of nodes.
*Implementations:*
val base_n_def = Define
`base_n (w1:real) (w2:real) (L1_n:real) (L2_n:real) = w1 * L1_n + w2 *
L2_n`;
val der_n_def = Define
`der_n (a:real) (b:real) (base_val_n:real) (L4_n:real) = base_val_n - a *
(L4_n - b)`;
val val_n_def = Define
`val_n (w1:real) (w2:real) (a:real) (b:real) (L1_n:real) (L2_n:real)
(L4_n:real)=
der_n a b (base_n w1 w2 L1_n L2_n) L4_n`;
val der_list_def = Define
`(*der_list* (w1:real) (w2:real) (a:real) (b:real) [] (L2_t:real list)
(L4_t:real list) = []) /\
(*der_list* w1 w2 a b ((L1_t_HD:real)::used_t_TL) L2_t L4_t =
val_n w1 w2 a b (L1_t_HD) (HD L2_t) (HD L4_t)
:: *der_list* w1 w2 a b (L1_t_TL) (TL L2_t) (TL L4_t))`;
val final_def = Define
`final (w1:real) (w2:real) (a:real) (b:real) (L1:num->(real list))
(L2:num->(real list)) (L4:num->(real list)) =
!t. *der_list* w1 w2 a b (L1 t) (L2 t) (L4 t)`;
The last function final gives type mismatch. When I make t:num as input to
the function, it works fine but I need to apply it for all times.
Help in this regard will be highly appreciated.
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/NeoTech
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
