|
--
-- Model of Digital ATC Database(1 & 2 /3) -- Track Circuits and Routes
--
-- ver 1. 2000.4.11 by n. terada
-- ver 2. 2000.6.14 by n. terada
-- ver 2.3 2000.6.26 by n. terada
-- ver 3 2000.8.16 by n. terada
-- ver 4 2000.9.13 by n. terada
-- ver 4.5 2000.9.15 by n. terada
-- ver 4.6 2000.10.11 by n. terada
-- ver 4.61 2001.2.5 by n.terada
-- track circuits -- basic unit
--
types
TrackC:: joints : map Joint_id to Joint
atc : map Direction to ATC
td : TD
atbt : ATBT
inv tc == card dom tc.joints > 1 and
dom tc.atc = {<ADIR>, <BDIR>} and
TD_Used_for_NonInsulated_TrackC(tc.td, tc.atbt, rng tc.joints) and
(tc.atc(<ADIR>).used and tc.atc(<BDIR>).used =>
tc.atc(<ADIR>).carrier <> tc.atc(<BDIR>).carrier);
--
-- joint -- connection between two track circuits
--
Joint_id = token;
Joint:: position : nat
insulated : Insulation
remark : Remark;
Insulation = bool; -- true if joint is insulated
Remark :: atc_terminal : map Direction to bool -- true if atc is terminated
line_terminal : bool -- true if line terminated
inv rm == dom rm.atc_terminal = {<ADIR>, <BDIR>};
Direction = <ADIR> | <BDIR>;
--
-- carrier of track circuits
-- atc signal , td(train detection signal)
--
ATC :: used : bool -- true if Digital ATC is used
carrier : token;
TD :: used : bool -- true if TD is used
carrier : token;
ATBT = <AT> | <BT> | <NULL>;
functions
TD_Used_for_NonInsulated_TrackC : TD * ATBT * set of Joint -> bool
TD_Used_for_NonInsulated_TrackC(td, atbt, joints) ==
(atbt = <NULL> <=> not td.used) and
((exists j in set joints & not j.insulated) => td.used);
--
-- Collection of Track Circuits
--
types
TrackC_id = token;
TrackC_map = map TrackC_id to TrackC
inv tcs == forall tid in set dom tcs &
forall jid in set dom tcs(tid).joints &
Only_One_Next_TrackC(tcs, tid, jid) and
forall tid2 in set dom tcs & tid <> tid2 =>
Joint_and_Next_TrackC(tcs(tid), tcs(tid2), jid)
;
functions
Only_One_Next_TrackC: map TrackC_id to TrackC * TrackC_id * Joint_id -> bool
Only_One_Next_TrackC(tcs, tcid, jid) ==
card {tid | tid in set dom tcs &
tid <> tcid and jid in set dom tcs(tid).joints} < 2;
Joint_and_Next_TrackC: TrackC * TrackC * Joint_id -> bool
Joint_and_Next_TrackC(tc1, tc2, jid) ==
(jid in set dom tc1.joints and jid in set dom tc2.joints) =>
(tc1.joints(jid) = tc2.joints(jid) and
not tc1.joints(jid).remark.line_terminal and
Is_wf_adjacent_signal(tc1, jid, tc2, jid, false));
--
-- condition related with signal
--
Is_wf_adjacent_signal: TrackC * Joint_id * TrackC * Joint_id * bool -> bool
Is_wf_adjacent_signal(tc1, jid1, tc2, jid2, dir_chng) ==
jid1 in set dom tc1.joints and
jid2 in set dom tc2.joints and
Remark_Compatible(tc1.joints(jid1).remark, tc2.joints(jid2).remark,
dir_chng) and
ATC_Terminal_and_ATC_Used(tc1.atc(<ADIR>), tc2.atc(<BDIR>),
tc1.joints(jid1).remark, tc2.atc(<ADIR>), tc2.atc(<BDIR>),
tc2.joints(jid2).remark, dir_chng) and
Adjacent_TD_Carrier_Differ(tc1.td, tc1.atbt, tc2.td, tc2.atbt,
tc1.joints(jid1).insulated and tc2.joints(jid2).insulated);
Remark_Compatible : Remark * Remark * bool-> bool
Remark_Compatible(rm1, rm2, dir_chng) ==
(not dir_chng => rm1.atc_terminal = rm2.atc_terminal) and
(dir_chng =>
(rm1.atc_terminal(<ADIR>) = rm2.atc_terminal(<BDIR>) and
rm1.atc_terminal(<BDIR>) = rm2.atc_terminal(<ADIR>)));
ATC_Terminal_and_ATC_Used : ATC * ATC * Remark * ATC * ATC * Remark * bool
-> bool
ATC_Terminal_and_ATC_Used(atcA1, atcB1, rm1, atcA2, atcB2, rm2, dir_chng) ==
(not dir_chng =>
(((atcA1.used <> atcA2.used) = rm1.atc_terminal(<ADIR>)) and
((atcB1.used <> atcB2.used) = rm1.atc_terminal(<BDIR>)))) and
(dir_chng =>
(((atcA1.used <> atcB2.used) = rm1.atc_terminal(<ADIR>)) and
((atcB1.used <> atcA2.used) = rm1.atc_terminal(<BDIR>))))
pre Remark_Compatible(rm1, rm2, dir_chng);
Adjacent_TD_Carrier_Differ : TD * ATBT * TD * ATBT * Insulation -> bool
Adjacent_TD_Carrier_Differ(td1, atbt1, td2, atbt2, insulated) ==
(insulated or
td1.carrier <> td2.carrier and
(atbt1 <> atbt2 or atbt1 = <AT> and atbt2 = <AT>));
--
-- end of track circuit
--
--
-- paths in track circuits
--
types
Path:: tc : TrackC_id
start : Joint_id
endp : Joint_id
length : nat
used : map Direction to bool
condition : set of Condition
inv p == p.start <> p.endp and
dom p.used = {<ADIR>, <BDIR>} and
(exists dr in set dom p.used & p.used(dr)) and
(forall c1, c2 in set p.condition & Condition_not_Conflict(c1, c2));
-- start.position < endp.position is added at inv_Area
Condition :: kind : Cond_Kind
start : nat
endp : nat
speed : nat -- only used for <LIMIT>
permill : nat -- should be integer or real
inv con == con.start < con.endp;
Cond_Kind = <LIMIT> | <GRADIENT> | <SECTION>;
functions
Condition_not_Conflict : Condition * Condition -> bool
Condition_not_Conflict(c1, c2) ==
(c1 <> c2 and c1.kind = c2.kind and c1.kind <> <LIMIT>) =>
not Overlap(c1, c2);
Overlap : Condition * Condition -> bool
Overlap(c1, c2) ==
(c1.start < c2.start and c2.start < c1.endp) or
(c2.start < c1.start and c1.start < c2.endp) or
(c1.start = c2.start)
;
types
Path_id = token;
Path_map = map Path_id to Path
inv ps == forall pid1, pid2 in set dom ps & pid1 <> pid2 =>
(Not_Same_Path(ps(pid1), ps(pid2)) and
Not_Start_and_End(ps(pid1), ps(pid2)));
functions
Not_Same_Path : Path * Path -> bool
Not_Same_Path(p1, p2) ==
not (p1.start = p2.start and p1.endp = p2.endp) and
not (p1.start = p2.endp and p1.endp = p2.start);
-- It is possible to allow the case p1.tc <> p2.tc
-- but that is not practical, so it is not allowed here.
Not_Start_and_End : Path * Path -> bool
Not_Start_and_End(p1, p2) ==
(p1.tc = p2.tc) =>
(not p1.start = p2.endp and not p2.start = p1.endp);
--
-- route
--
types
Route:: dr : Direction
paths : seq1 of Path_id;
Route_map = map Route_id to Route
;
Route_id = token;
--
-- Area -- corresponds to stations or intermediate part.
--
Area :: trackcs : TrackC_map
paths : Path_map
routes : Route_map
kind : Area_Kind
max : MaxSpeed
inv mk_Area(trackcs, paths, routes, -, -) ==
(forall p in set rng paths &
Path_within_TrackC(trackcs, p) and
Direction_Correct(trackcs, p)) and
(forall r in set rng routes &
Path_Exists(paths, r.paths, r.dr) and
Exists_ATC_for_Route(trackcs, paths, r) and
Route_not_Circular(paths, r) and
Path_Connected(paths, r.paths, r.dr))
;
Area_Kind = <PLAIN> | <COMPLEX>;
MaxSpeed = token;
functions
Path_within_TrackC : TrackC_map * Path -> bool
Path_within_TrackC(trackcs, p) ==
p.tc in set dom trackcs and
p.start in set dom trackcs(p.tc).joints and
p.endp in set dom trackcs(p.tc).joints
;
Direction_Correct : TrackC_map * Path -> bool
Direction_Correct(trackcs, p) ==
let pstart = trackcs(p.tc).joints(p.start).position,
pend = trackcs(p.tc).joints(p.endp).position in
pstart < pend and
p.length = pend - pstart and
forall c in set p.condition &
pstart <= c.start and c.endp <= pend
pre Path_within_TrackC(trackcs, p);
Path_Exists : Path_map * seq of Path_id * Direction -> bool
Path_Exists(paths, route, dr) ==
forall pid in seq route &
pid in set dom paths and
paths(pid).used(dr)
;
-- next function is related with signal
Exists_ATC_for_Route : TrackC_map * Path_map * Route -> bool
Exists_ATC_for_Route(trackcs, paths, r) ==
forall pid in seq r.paths &
paths(pid).tc in set dom trackcs and
trackcs(paths(pid).tc).atc(r.dr).used
pre Path_Exists(paths, r.paths, r.dr);
Route_not_Circular : Path_map * Route-> bool
Route_not_Circular(paths, r) ==
forall i, j in set inds r.paths &
i <> j => paths(r.paths(i)).tc <> paths(r.paths(j)).tc
pre Path_Exists(paths, r.paths, r.dr);
Path_Connected : Path_map * seq of Path_id * Direction-> bool
Path_Connected(paths, route, dr) ==
forall i in set inds route &
(i + 1) in set inds route =>
((dr = <ADIR> =>
paths(route(i)).endp = paths(route(i+1)).start) and
(dr = <BDIR> =>
paths(route(i)).start = paths(route(i+1)).endp))
pre Path_Exists(paths, route, dr);
--
-- end of invariant
--
--
-- Operation of Data Base (Area Level)
--
Add_TrackC : Area * TrackC_id * TrackC -> Area
Add_TrackC(ar, tcid, tc) ==
mu(ar, trackcs |-> ar.trackcs ++ {tcid |-> tc})
pre tcid not in set dom ar.trackcs and
forall jid in set dom tc.joints &
Only_One_Next_TrackC(ar.trackcs, tcid, jid) and
forall tcid1 in set dom ar.trackcs &
Joint_and_Next_TrackC(tc, ar.trackcs(tcid1), jid)
post tcid in set dom RESULT.trackcs and
RESULT.trackcs = ar.trackcs ++ {tcid |-> tc} and
RESULT.trackcs(tcid) = tc and
RESULT.paths = ar.paths and
RESULT.routes = ar.routes;
Del_TrackC : Area * TrackC_id -> Area
Del_TrackC(ar, tcid) ==
mu(ar, trackcs |-> {tcid} <-: ar.trackcs)
pre tcid in set dom ar.trackcs and
forall p in set rng ar.paths & p.tc <> tcid
post tcid not in set dom RESULT.trackcs and
RESULT.trackcs = {tcid} <-: ar.trackcs and
RESULT.paths = ar.paths and
RESULT.routes = ar.routes;
Add_Joint : Area * TrackC_id * Joint_id * Joint -> Area
Add_Joint(ar, tid, jid, joint) ==
let tc = ar.trackcs(tid) in
mu(ar, trackcs |-> ar.trackcs ++ {tid |->
mu(tc, joints |-> tc.joints ++ {jid |-> joint})})
pre tid in set dom ar.trackcs and
let tc = ar.trackcs(tid) in
jid not in set dom tc.joints and
TD_Used_for_NonInsulated_TrackC(tc.td, tc.atbt,
rng tc.joints union {joint}) and
Only_One_Next_TrackC(ar.trackcs, tid, jid) and
forall tid1 in set dom ar.trackcs & tid1 <> tid =>
Joint_and_Next_TrackC(ar.trackcs(tid1),
mu(tc,joints |-> tc.joints ++ {jid |-> joint}), jid)
post tid in set dom RESULT.trackcs and
jid in set dom RESULT.trackcs(tid).joints and
dom RESULT.trackcs = dom ar.trackcs and
{tid} <-: RESULT.trackcs = {tid} <-: ar.trackcs and
RESULT.trackcs(tid) = mu(ar.trackcs(tid),
joints |-> ar.trackcs(tid).joints ++ {jid |-> joint}) and
RESULT.trackcs(tid).joints(jid) = joint and
RESULT.trackcs(tid).atc = ar.trackcs(tid).atc and
RESULT.trackcs(tid).td = ar.trackcs(tid).td and
RESULT.trackcs(tid).atbt = ar.trackcs(tid).atbt and
RESULT.paths = ar.paths and
RESULT.routes = ar.routes
;
Del_Joint : Area * TrackC_id * Joint_id -> Area
Del_Joint(ar, tcid, jid) ==
let tc = ar.trackcs(tcid) in
mu(ar, trackcs |-> ar.trackcs ++
{tcid |-> mu(tc, joints |-> {jid} <-: tc.joints)})
pre tcid in set dom ar.trackcs and
jid in set dom ar.trackcs(tcid).joints and
card dom ar.trackcs(tcid).joints > 2 and
(forall path in set rng ar.paths &
path.tc <> tcid or
jid <> path.start and jid <> path.endp)
post tcid in set dom RESULT.trackcs and
dom RESULT.trackcs = dom ar.trackcs and
{tcid} <-: RESULT.trackcs = {tcid} <-: ar.trackcs and
jid not in set dom RESULT.trackcs(tcid).joints and
RESULT.trackcs(tcid) = mu(ar.trackcs(tcid),
joints |-> {jid} <-: ar.trackcs(tcid).joints) and
RESULT.trackcs(tcid).atc = ar.trackcs(tcid).atc and
RESULT.trackcs(tcid).td = ar.trackcs(tcid).td and
RESULT.trackcs(tcid).atbt = ar.trackcs(tcid).atbt and
RESULT.trackcs(tcid).joints = {jid} <-: ar.trackcs(tcid).joints and
RESULT.paths = ar.paths and
RESULT.routes = ar.routes
;
Add_Path : Area * Path_id * Path -> Area
Add_Path(ar, pid, path) ==
mu(ar, paths |-> ar.paths ++ {pid |-> path})
pre pid not in set dom ar.paths and
Path_within_TrackC(ar.trackcs, path) and
Direction_Correct(ar.trackcs, path) and
forall p in set rng ar.paths &
Not_Same_Path(p, path) and Not_Start_and_End(p, path)
post pid in set dom RESULT.paths and
RESULT.paths = ar.paths ++ {pid |-> path} and
RESULT.paths(pid) = path and
RESULT.trackcs = ar.trackcs and
RESULT.routes = ar.routes;
Del_Path : Area * Path_id -> Area
Del_Path(ar, pid) ==
mu(ar, paths |-> {pid} <-: ar.paths)
pre pid in set dom ar.paths and
forall r in set rng ar.routes & pid not in set elems r.paths
post pid not in set dom RESULT.paths and
RESULT.paths = {pid} <-: ar.paths and
RESULT.trackcs = ar.trackcs and
RESULT.routes = ar.routes;
Add_Route : Area * Route_id * Route -> Area
Add_Route (ar, rid, r) ==
mu(ar, routes |-> ar.routes ++ {rid |-> r})
pre rid not in set dom ar.routes and
Path_Exists(ar.paths, r.paths, r.dr) and
Exists_ATC_for_Route(ar.trackcs, ar.paths, r) and
Route_not_Circular(ar.paths, r) and
Path_Connected(ar.paths, r.paths, r.dr)
post rid in set dom RESULT.routes and
RESULT.routes = ar.routes ++ {rid |-> r} and
RESULT.routes(rid) = r and
RESULT.trackcs = ar.trackcs and
RESULT.paths = ar.paths;
Del_Route : Area * Route_id -> Area
Del_Route(ar, rid) ==
mu(ar, routes |-> {rid} <-: ar.routes)
pre rid in set dom ar.routes
post rid not in set dom RESULT.routes and
RESULT.routes = {rid} <-: ar.routes and
RESULT.trackcs = ar.trackcs and
RESULT.paths = ar.paths;
Add_Condition : Area * Path_id * Condition -> Area
Add_Condition(ar, pid, con) ==
let p = mu(ar.paths(pid),
condition |-> ar.paths(pid).condition union {con}) in
mu(ar, paths |-> ar.paths ++ {pid |-> p})
pre pid in set dom ar.paths and
let p = ar.paths(pid) in
ar.trackcs(p.tc).joints(p.start).position <= con.start and
con.endp <= ar.trackcs(p.tc).joints(p.endp).position and
(forall c in set p.condition & Condition_not_Conflict(c, con))
post pid in set dom RESULT.paths and
dom RESULT.paths = dom ar.paths and
{pid} <-: RESULT.paths = {pid} <-: ar.paths and
RESULT.paths(pid) = mu(ar.paths(pid),
condition |-> ar.paths(pid).condition union {con}) and
RESULT.paths(pid).start = ar.paths(pid).start and
RESULT.paths(pid).endp = ar.paths(pid).endp and
RESULT.paths(pid).tc = ar.paths(pid).tc and
RESULT.paths(pid).length = ar.paths(pid).length and
RESULT.paths(pid).condition = ar.paths(pid).condition union {con} and
RESULT.trackcs = ar.trackcs and
RESULT.routes = ar.routes
;
Del_Condition : Area * Path_id * Cond_Kind * nat * nat -> Area
Del_Condition(ar, pid, kind, start, endp) ==
let p = mu(ar.paths(pid), condition |->
{l | l in set ar.paths(pid).condition &
not (l.kind = kind and l.start = start and l.endp = endp)}) in
mu(ar, paths |-> ar.paths ++ {pid |-> p})
pre pid in set dom ar.paths and
(exists c in set ar.paths(pid).condition &
c.kind = kind and c.start = start and c.endp = endp)
post pid in set dom RESULT.paths and
dom RESULT.paths = dom ar.paths and
{pid} <-: RESULT.paths = {pid} <-: ar.paths and
RESULT.paths(pid) = mu(ar.paths(pid), condition |->
{l | l in set ar.paths(pid).condition &
not (l.kind = kind and l.start = start and l.endp = endp)}) and
RESULT.paths(pid).start = ar.paths(pid).start and
RESULT.paths(pid).endp = ar.paths(pid).endp and
RESULT.paths(pid).tc = ar.paths(pid).tc and
RESULT.paths(pid).length = ar.paths(pid).length and
RESULT.trackcs = ar.trackcs and
RESULT.routes = ar.routes
;
--
-- end of Operation (Area level)
--
types
--
-- Line -- collection of Areas
--
--
Line :: areas : Area_map
connect : Connect_map
-- ver : Version --
-- edit_date : Date -- These 4 fields are
-- valid_date : Date -- to be used version control system.
-- locked : bool --
inv mk_Line(areas, connect) ==
forall c in set dom connect &
(forall n in set c & Area_Joint_Exists(areas, n)) and
(forall n1, n2 in set c & n1 <> n2 =>
Direction_for_Area_Joint(areas(n1.aid).paths, n1.no,
areas(n2.aid).paths, n2.no, connect(c).chng_direction) and
let tc1 = areas(n1.aid).trackcs(n1.tcid),
tc2 = areas(n2.aid).trackcs(n2.tcid) in
Joint_Compatible(tc1.joints(n1.no), tc2.joints(n2.no),
connect(c)) and
Is_wf_adjacent_signal(tc1, n1.no, tc2, n2.no,
connect(c).chng_direction));
Area_map = map Area_id to Area;
Area_id = token;
-- (Plan)
-- Area_id :: lid : nat
-- aid : nat
--
-- connection between two areas
--
Area_Joint :: aid : Area_id
tcid : TrackC_id
no : Joint_id;
Connect = set of Area_Joint
inv con == card con = 2 and
forall a1, a2 in set con & a1 <> a2 => a1.aid <> a2.aid;
Connect_map = map Connect to Remark_Connect
inv con == forall a1, a2 in set dom con & a1 <> a2 => a1 inter a2 = {};
Remark_Connect :: chng_direction : bool
chng_distance : bool;
functions
Area_Joint_Exists : Area_map * Area_Joint -> bool
Area_Joint_Exists(areas, n) ==
n.aid in set dom areas and
n.tcid in set dom areas(n.aid).trackcs and
n.no in set dom areas(n.aid).trackcs(n.tcid).joints and
not areas(n.aid).trackcs(n.tcid).joints(n.no).remark.line_terminal and
forall tcid in set dom areas(n.aid).trackcs & n.tcid <> tcid =>
n.no not in set dom areas(n.aid).trackcs(tcid).joints;
Direction_for_Area_Joint : Path_map * Joint_id * Path_map * Joint_id * bool
-> bool
Direction_for_Area_Joint(pm1, n1, pm2, n2, chng_dir) ==
forall p1 in set rng pm1, p2 in set rng pm2 &
((p1.start = n1 and p2.start = n2) => chng_dir) and
((p1.endp = n1 and p2.endp = n2) => chng_dir) and
((p1.start = n1 and p2.endp = n2) => not chng_dir) and
((p1.endp = n1 and p2.start = n2) => not chng_dir)
;
Joint_Compatible: Joint * Joint * Remark_Connect -> bool
Joint_Compatible(j1, j2, rm) ==
j1.insulated = j2.insulated and
((j1.position <> j2.position) = rm.chng_distance) and
Remark_Compatible(j1.remark, j2.remark, rm.chng_direction);
Add_Area : Line * Area_id * Area_Kind * MaxSpeed -> Line
Add_Area(ln, aid, kind, max) ==
mu(ln, areas |-> ln.areas ++ {aid |-> mk_Area({|->}, {|->}, {|->}, kind, max)})
pre aid not in set dom ln.areas
post aid in set dom RESULT.areas and
RESULT.connect = ln.connect;
Change_Area : Line * Area_id * Area -> Line
Change_Area(ln, aid, area) ==
mu(ln, areas |-> ln.areas ++ {aid |-> area})
pre aid in set dom ln.areas and
inv_Line(mk_Line(ln.areas ++ {aid |-> area}, ln.connect))
post RESULT.areas(aid) = area and
RESULT.connect = ln.connect;
Del_Area : Line * Area_id -> Line
Del_Area(ln, aid) ==
mu(ln, areas |-> {aid} <-: ln.areas)
pre aid in set dom ln.areas and
(forall c in set dom ln.connect &
forall aj in set c & aj.aid <> aid)
post aid not in set dom RESULT.areas and
RESULT.connect = ln.connect;
Add_Connect : Line * Connect * Remark_Connect -> Line
Add_Connect(ln, con, r) ==
mu(ln, connect |-> ln.connect ++ {con |-> r})
pre (forall c in set dom ln.connect & c inter con = {}) and
(forall n in set con & Area_Joint_Exists(ln.areas, n)) and
(forall n1, n2 in set con & n1 <> n2 =>
Direction_for_Area_Joint(ln.areas(n1.aid).paths, n1.no,
ln.areas(n2.aid).paths, n2.no, r.chng_direction) and
let tc1 = ln.areas(n1.aid).trackcs(n1.tcid),
tc2 = ln.areas(n2.aid).trackcs(n2.tcid) in
Joint_Compatible(tc1.joints(n1.no), tc2.joints(n2.no), r) and
Is_wf_adjacent_signal(tc1,n1.no, tc2, n2.no, r.chng_direction))
post con in set dom RESULT.connect and
RESULT.connect = ln.connect ++ {con |-> r} and
RESULT.connect(con) = r and
RESULT.areas = ln.areas
;
Del_Connect : Line * Area_Joint -> Line
Del_Connect(ln, n) ==
mu(ln, connect |->
{c |-> ln.connect(c) | c in set dom ln.connect & n not in set c})
pre exists c in set dom ln.connect & n in set c
post forall c in set dom RESULT.connect & n not in set c and
RESULT.areas = ln.areas;
functions
Line_Add_TrackC : Line * Area_id * TrackC_id * TrackC -> Line
Line_Add_TrackC(ln, aid, tcid, tc) ==
mu(ln, areas |-> ln.areas ++
{aid |-> Add_TrackC(ln.areas(aid), tcid, tc)})
pre aid in set dom ln.areas and
pre_Add_TrackC(ln.areas(aid), tcid, tc) and
(forall jid in set dom tc.joints &
forall c in set dom ln.connect &
forall n in set c &
n.aid = aid => n.no <> jid)
post aid in set dom RESULT.areas and
dom ln.areas = dom RESULT.areas and
{aid} <-: RESULT.areas = {aid} <-: ln.areas and
tcid in set dom RESULT.areas(aid).trackcs and
RESULT.areas(aid).trackcs =
ln.areas(aid).trackcs ++ {tcid |-> tc} and
RESULT.areas(aid).trackcs(tcid) = tc and
RESULT.connect = ln.connect;
Line_Del_TrackC : Line * Area_id * TrackC_id -> Line
Line_Del_TrackC(ln, aid, tcid) ==
mu(ln, areas |-> ln.areas ++
{aid |-> Del_TrackC(ln.areas(aid), tcid)})
pre aid in set dom ln.areas and
pre_Del_TrackC(ln.areas(aid), tcid) and
forall c in set dom ln.connect & forall aj in set c &
aj.aid = aid => aj.tcid <> tcid
post aid in set dom RESULT.areas and
dom ln.areas = dom RESULT.areas and
{aid} <-: RESULT.areas = {aid} <-: ln.areas and
RESULT.areas(aid).trackcs = {tcid} <-: ln.areas(aid).trackcs and
tcid not in set dom RESULT.areas(aid).trackcs and
RESULT.connect = ln.connect;
Line_Add_Joint : Line * Area_id * TrackC_id * Joint_id * Joint -> Line
Line_Add_Joint(ln, aid, tcid, jid, j) ==
mu(ln, areas |-> ln.areas ++
{aid |-> Add_Joint(ln.areas(aid), tcid, jid, j)})
pre aid in set dom ln.areas and
pre_Add_Joint(ln.areas(aid), tcid, jid, j) and
(forall c in set dom ln.connect & forall n in set c &
n.aid = aid => n.no <> jid)
post aid in set dom RESULT.areas and
tcid in set dom RESULT.areas(aid).trackcs and
jid in set dom RESULT.areas(aid).trackcs(tcid).joints and
dom RESULT.areas = dom ln.areas and
{aid} <-: RESULT.areas = {aid} <-: ln.areas and
dom RESULT.areas(aid).trackcs = dom ln.areas(aid).trackcs and
{tcid} <-: RESULT.areas(aid).trackcs =
{tcid} <-: ln.areas(aid).trackcs and
RESULT.areas(aid).trackcs(tcid).joints =
ln.areas(aid).trackcs(tcid).joints ++ {jid |-> j} and
RESULT.areas(aid).trackcs(tcid).joints(jid) = j and
RESULT.connect = ln.connect;
Line_Del_Joint : Line * Area_id * TrackC_id * Joint_id -> Line
Line_Del_Joint(ln, aid, tcid, jid) ==
mu(ln, areas |-> ln.areas ++
{aid |-> Del_Joint(ln.areas(aid), tcid, jid)})
pre aid in set dom ln.areas and
pre_Del_Joint(ln.areas(aid), tcid, jid) and
forall c in set dom ln.connect & forall aj in set c &
(aj.aid = aid and aj.tcid = tcid) => aj.no <> jid
post aid in set dom RESULT.areas and
tcid in set dom RESULT.areas(aid).trackcs and
jid not in set dom RESULT.areas(aid).trackcs(tcid).joints and
dom RESULT.areas = dom ln.areas and
{aid} <-: RESULT.areas = {aid} <-: ln.areas and
dom RESULT.areas(aid).trackcs = dom ln.areas(aid).trackcs and
{tcid} <-: RESULT.areas(aid).trackcs =
{tcid} <-: ln.areas(aid).trackcs and
RESULT.areas(aid).trackcs(tcid).joints =
{jid} <-: ln.areas(aid).trackcs(tcid).joints and
RESULT.connect = ln.connect;
Line_Add_Path : Line * Area_id * Path_id * Path -> Line
Line_Add_Path(ln, aid, pid, p) ==
mu(ln, areas |-> ln.areas ++
{aid |-> Add_Path(ln.areas(aid), pid, p)})
pre aid in set dom ln.areas and
pre_Add_Path(ln.areas(aid), pid, p) and
forall c in set dom ln.connect &
forall n1, n2 in set c &
(n1 <> n2 and n1.aid = aid) =>
Direction_for_Area_Joint({pid |-> p}, n1.no,
ln.areas(n2.aid).paths , n2.no, ln.connect(c).chng_direction)
post aid in set dom RESULT.areas and
pid in set dom RESULT.areas(aid).paths and
dom RESULT.areas = dom ln.areas and
{aid} <-: RESULT.areas = {aid} <-: ln.areas and
RESULT.areas(aid).paths = ln.areas(aid).paths ++ {pid |-> p} and
RESULT.areas(aid).paths(pid) = p and
RESULT.connect = ln.connect;
Line_Del_Path : Line * Area_id * Path_id -> Line
Line_Del_Path(ln, aid, pid) ==
mu(ln, areas |-> ln.areas ++ {aid |-> Del_Path(ln.areas(aid), pid)})
pre aid in set dom ln.areas and
pre_Del_Path(ln.areas(aid), pid)
post aid in set dom RESULT.areas and
pid not in set dom RESULT.areas(aid).paths and
dom RESULT.areas = dom ln.areas and
{aid} <-: RESULT.areas = {aid} <-: ln.areas and
RESULT.areas(aid).paths = {pid} <-: ln.areas(aid).paths and
RESULT.connect = ln.connect;
Line_Add_Route : Line * Area_id * Route_id * Route -> Line
Line_Add_Route(ln, aid, rid, r) ==
mu(ln, areas |-> ln.areas ++ {aid |-> Add_Route(ln.areas(aid), rid,r)})
pre aid in set dom ln.areas and
pre_Add_Route(ln.areas(aid), rid, r)
post aid in set dom RESULT.areas and
rid in set dom RESULT.areas(aid).routes and
dom RESULT.areas = dom ln.areas and
{aid} <-: RESULT.areas = {aid} <-: ln.areas and
RESULT.areas(aid).routes = ln.areas(aid).routes ++ {rid |-> r} and
RESULT.areas(aid).routes(rid) = r and
RESULT.connect = ln.connect;
Line_Del_Route : Line * Area_id * Route_id -> Line
Line_Del_Route(ln, aid, rid) ==
mu(ln, areas |-> ln.areas ++ {aid |-> Del_Route(ln.areas(aid), rid)})
pre aid in set dom ln.areas and
pre_Del_Route(ln.areas(aid), rid)
post aid in set dom RESULT.areas and
dom RESULT.areas = dom ln.areas and
{aid} <-: RESULT.areas = {aid} <-: ln.areas and
rid not in set dom RESULT.areas(aid).routes and
RESULT.areas(aid).routes = {rid} <-: ln.areas(aid).routes and
RESULT.connect = ln.connect;
Line_Add_Condition : Line * Area_id * Path_id * Condition-> Line
Line_Add_Condition(ln, aid, pid, con) ==
mu(ln, areas |-> ln.areas ++
{aid |-> Add_Condition(ln.areas(aid), pid, con)})
pre aid in set dom ln.areas and
pre_Add_Condition(ln.areas(aid), pid, con);
Line_Del_Condition : Line * Area_id * Path_id * Cond_Kind * nat * nat-> Line
Line_Del_Condition(ln, aid, pid, kind, start, endp) ==
mu(ln, areas |-> ln.areas ++
{aid |-> Del_Condition(ln.areas(aid), pid, kind, start, endp)})
pre aid in set dom ln.areas and
pre_Del_Condition(ln.areas(aid), pid, kind, start, endp)
;
--
-- Digital ATC Database
-- Condition for "Completed" Database
--
functions
Is_wf_Line_DB : Line -> bool
Is_wf_Line_DB(ln) ==
(forall aid in set dom ln.areas & let ar = ln.areas(aid) in
Joint_Completed(ar.trackcs, aid, ln.connect) and
Path_Exists_for_Joint(ar.trackcs, ar.paths) and
Path_Exists_for_TrackC(ar.trackcs, ar.paths) and
Route_Exists_for_Path(ar) and
Path_Exists_before_Start(ar, aid, ln.connect) and
Path_Exists_after_End(ar, aid, ln.connect) and
Route_Exists_to_Terminal(ar, aid, ln.connect) and
(ar.kind = <PLAIN> => Is_Plain_Area(ar, aid, ln.connect))) and
Following_Path_Exists_at_Connect(ln) and
Preceding_Path_Exists_at_Connect(ln) and
One_Side_Unique_Path_at_Connection(ln);
Joint_Completed : TrackC_map * Area_id * Connect_map -> bool
Joint_Completed(trackcs, aid, connect) ==
forall tid in set dom trackcs &
let tc = trackcs(tid) in
forall jid in set dom tc.joints &
(not exists tcid in set dom trackcs & tcid <> tid and
jid in set dom trackcs(tcid).joints) =>
(mk_Area_Joint(aid, tid, jid) in set dunion dom connect or
tc.joints(jid).remark.line_terminal)
;
Path_Exists_for_Joint : TrackC_map * Path_map -> bool
Path_Exists_for_Joint(trackcs, paths) ==
forall tid in set dom trackcs &
forall jid in set dom trackcs(tid).joints &
(exists p in set rng paths &
p.tc = tid and
(p.start = jid or p.endp = jid))
;
Path_Exists_for_TrackC : TrackC_map * Path_map -> bool
Path_Exists_for_TrackC(trackcs, paths) ==
forall tid in set dom trackcs &
forall dr in set dom trackcs(tid).atc &
trackcs(tid).atc(dr).used =>
exists p in set rng paths &
p.tc = tid and p.used(dr)
;
Route_Exists_for_Path : Area -> bool
Route_Exists_for_Path(ar) ==
forall pid in set dom ar.paths &
forall dr in set dom ar.paths(pid).used &
ar.paths(pid).used(dr) =>
ar.trackcs(ar.paths(pid).tc).atc(dr).used =>
exists r in set rng ar.routes &
r.dr = dr and pid in set elems r.paths;
Path_Exists_before_Start : Area * Area_id * Connect_map -> bool
Path_Exists_before_Start(ar, aid, connect) ==
forall pid in set dom ar.paths &
let p = ar.paths(pid) in
forall dr in set dom p.used &
p.used(dr) =>
(mk_Area_Joint(aid, p.tc, p.start) in set dunion dom connect or
ar.trackcs(p.tc).joints(p.start).remark.line_terminal or
ar.trackcs(p.tc).joints(p.start).remark.atc_terminal(dr) or
exists pid1 in set dom ar.paths &
let p1 = ar.paths(pid1) in
p1.tc <> p.tc and
p1.used(dr) and
p1.endp = p.start)
;
Path_Exists_after_End : Area * Area_id * Connect_map -> bool
Path_Exists_after_End(ar, aid, connect) ==
forall pid in set dom ar.paths &
let p = ar.paths(pid) in
forall dr in set dom p.used &
p.used(dr) =>
(mk_Area_Joint(aid, p.tc, p.endp) in set dunion dom connect or
ar.trackcs(p.tc).joints(p.endp).remark.line_terminal or
ar.trackcs(p.tc).joints(p.endp).remark.atc_terminal(dr) or
exists pid1 in set dom ar.paths &
let p1 = ar.paths(pid1) in
p1.tc <> p.tc and
p1.used(dr) and
p1.start = p.endp)
;
StartJoint : Path * Direction -> Joint_id
StartJoint(path, dr) ==
if dr = <ADIR> then path.start else path.endp
post (dr = <ADIR> => RESULT = path.start) and
(dr = <BDIR> => RESULT = path.endp);
EndJoint : Path * Direction -> Joint_id
EndJoint(path, dr) ==
if dr = <ADIR> then path.endp else path.start
post (dr = <ADIR> => RESULT = path.endp) and
(dr = <BDIR> => RESULT = path.start);
--
-- Route_Exists_to_Terminal means that Train can reach an Area_Joint or
-- an end of track.
Route_Exists_to_Terminal : Area * Area_id * Connect_map -> bool
Route_Exists_to_Terminal(ar, aid, connect) ==
forall rid in set dom ar.routes &
let r = ar.routes(rid) in
let pid = r.paths(len r.paths) in
let jid = EndJoint(ar.paths(pid), r.dr),
tcid = ar.paths(pid).tc in
mk_Area_Joint(aid, tcid, jid) in set dunion dom connect or
ar.trackcs(tcid).joints(jid).remark.line_terminal or
ar.trackcs(tcid).joints(jid).remark.atc_terminal(r.dr) or
Following_Route_Exists(ar.routes, rid) or
Following_Path_Unique(ar.paths, pid, r.dr);
--
-- Following_Route_Exists1 :
-- On the last path, if a next route which includes following paths can
-- be indicated, train can proceed with next route ID.
--
Following_Route_Exists : Route_map * Route_id -> bool
Following_Route_Exists(routes, rid) ==
exists rid1 in set dom routes &
let r = routes(rid), r1 = routes(rid1) in
r1.dr = r.dr and
exists i in set inds r1.paths &
r1.paths(i) = r.paths(len r.paths) and
i < len r1.paths
pre rid in set dom routes;
--
-- Unique_Next_Path :
-- On the last path, if there is only one next path possible,
-- trains can proceed to the next path.
--
Following_Path_Unique : Path_map * Path_id * Direction-> bool
Following_Path_Unique(paths, pid, dr) ==
exists1 pid1 in set dom paths &
paths(pid1).tc <> paths(pid).tc and
paths(pid1).used(dr) and
EndJoint(paths(pid), dr) = StartJoint(paths(pid1), dr)
pre pid in set dom paths;
--
-- Plain Area, where from TrackC_id and direction, Route can be determined.
--
Is_Plain_Area : Area * Area_id * Connect_map-> bool
Is_Plain_Area(ar, aid, connect) ==
(forall tcid in set dom ar.trackcs &
forall dr in set dom ar.trackcs(tcid).atc &
ar.trackcs(tcid).atc(dr).used =>
exists1 rid in set dom ar.routes &
ar.routes(rid).dr = dr and
exists pid in seq ar.routes(rid).paths &
ar.paths(pid).tc = tcid) and
(forall r in set rng ar.routes &
let p = ar.paths(r.paths(len r.paths)) in
let jid = EndJoint(p, r.dr) in
mk_Area_Joint(aid, p.tc, jid) in set dunion dom connect or
ar.trackcs(p.tc).joints(jid).remark.line_terminal or
ar.trackcs(p.tc).joints(jid).remark.atc_terminal(r.dr));
--
-- One_Side_Unique_Path_at_Connection
-- At the connection it is not favorable that
-- in both area paths are not unique.
-- Because it makes imposibble to indicate next path
-- in the former track circuit.
One_Side_Unique_Path_at_Connection : Line -> bool
One_Side_Unique_Path_at_Connection(ln) ==
forall con in set dom ln.connect &
forall n1, n2 in set con & n1 <> n2 =>
forall dr in set {<ADIR>, <BDIR>} &
card {p | p in set rng ln.areas(n1.aid).paths &
p.used(dr) and
EndJoint(p, dr) = n1.no} > 1 =>
(ln.areas(n1.aid).trackcs(n1.tcid).joints(n1.no).
remark.atc_terminal(dr) or
let dr2 = if not ln.connect(con).chng_direction then dr
else if dr = <ADIR> then <BDIR> else <ADIR> in
card {p | p in set rng ln.areas(n2.aid).paths &
p.used(dr2) and
StartJoint(p, dr2) = n2.no} = 1);
Following_Path_Exists_at_Connect : Line -> bool
Following_Path_Exists_at_Connect(ln) ==
forall con in set dom ln.connect &
forall n1, n2 in set con & n1 <> n2 =>
forall dr in set {<ADIR>, <BDIR>} &
(exists p in set rng ln.areas(n1.aid).paths &
p.used(dr) and
EndJoint(p, dr) = n1.no) =>
(ln.areas(n1.aid).trackcs(n1.tcid).joints(n1.no).
remark.atc_terminal(dr) or
(exists p2 in set rng ln.areas(n2.aid).paths &
let dr2 = if not ln.connect(con).chng_direction then dr
else if dr = <ADIR> then <BDIR> else <ADIR> in
p2.used(dr2) and
StartJoint(p2, dr2) = n2.no));
Preceding_Path_Exists_at_Connect : Line -> bool
Preceding_Path_Exists_at_Connect(ln) ==
forall con in set dom ln.connect &
forall n1, n2 in set con & n1 <> n2 =>
forall dr in set {<ADIR>, <BDIR>} &
(exists p in set rng ln.areas(n1.aid).paths &
p.used(dr) and
StartJoint(p, dr) = n1.no) =>
(ln.areas(n1.aid).trackcs(n1.tcid).joints(n1.no).
remark.atc_terminal(dr) or
(exists p2 in set rng ln.areas(n2.aid).paths &
let dr2 = if not ln.connect(con).chng_direction
then dr
elseif dr = <ADIR>
then <BDIR>
else <ADIR> in
p2.used(dr2) and
EndJoint(p2, dr2) = n2.no));
¤ Dauer der Verarbeitung: 0.47 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
