|
%********************************************************************************%
%
% Contributions from:
%
% Andréia Borges Avelar -- Universidade de Brasília - Brasil
% Mauricio Ayala-Rincon -- Universidade de Brasília - Brasil
% Cesar Muñoz -- NASA Langley Research Center - US
%
%********************************************************************************%
wgt_digraphs_props[T : TYPE, Weight : TYPE,
+ : {f : [[Weight, Weight] -> Weight] |
commutative?(f) AND associative?(f) },
0 : {zero: Weight | identity?(+)(zero)},
<= : {<=: (partial_order?[Weight]) | FORALL(a, b, c : Weight):
a + b <= a + c => b <= c}
] : THEORY
BEGIN
IMPORTING weighted_digraphs[T, Weight, +, 0]
G : VAR wdg
u, v : VAR T
% ----------------------------------------------------------------------------- %
% DEFINITIONS: about minimun weights
% ----------------------------------------------------------------------------- %
min_walk?(G, u, v)( w: Walk(dg(G))) : bool =
FORALL(w1: Walk(dg(G)) | from?(w1, u, v)):
wgt_walk(G, w) <= wgt_walk(G, w1)
set_min(G)(u, v): set[Walk(dg(G))] =
{w: Walk(dg(G)) | from?(w, u, v) AND min_walk?(G, u, v)(w)}
min_wgt(G)(e: edgetype | nonempty?(set_min(G)(e))): Weight =
wgt_walk(G, choose(set_min(G)(e)))
% ----------------------------------------------------------------------------- %
% More properties on weighted digraphs that require
% a partial order, commutativity and homogeneity
% ----------------------------------------------------------------------------- %
walk_member_set_min: LEMMA
FORALL (w: Walk(dg(G)), e: edgetype | nonempty?(set_min(G)(e))):
from?(w, e`1, e`2) AND wgt_walk(G, w) = min_wgt(G)(e)
IMPLIES member(w, set_min(G)(e))
wgt_min_walk_choose: LEMMA
FORALL (w: Walk(dg(G))):
member(w, set_min(G)(u, v)) IMPLIES
wgt_walk(G, w) = wgt_walk(G, choose(set_min(G)(u, v)))
min_walk_min_wgt: LEMMA
FORALL (w: Walk(dg(G))):
member(w, set_min(G)(u, v)) IMPLIES
wgt_walk(G, w) = min_wgt(G)(u, v)
sub_min_walk_nonempty: LEMMA
FORALL(w: Walk(dg(G)),
e: edgetype | nonempty?(set_min(G)(e)),
i, j: below(length(w))):
walk_from?(dg(G), w, e`1, e`2) AND wgt_walk(G, w) = min_wgt(G)(e) AND i < j
IMPLIES
nonempty?( set_min(G)( w(i), w(j) ) )
sub_min_walk_is_min: LEMMA
FORALL(w: Walk(dg(G)),
e: edgetype | nonempty?(set_min(G)(e)),
i, j: below(length(w)) ):
walk_from?(dg(G), w, e`1, e`2) AND wgt_walk(G, w) = min_wgt(G)(e) AND i < j
IMPLIES
wgt_walk(G, w^(i,j)) = min_wgt(G)(w(i), w(j))
END wgt_digraphs_props
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
