% File: rcs1 % First Release date: 9/30/00 % % $Name: $ % %--------------------------------------------------------------------- % FORWARD RCS FLUID CONTROL SYSTEM %--------------------------------------------------------------------- % % The Fluid Control System is subdivided into: % a. Hydraulic System % b. Valve Control System % %--------------------------------------------------------------------- %%%%%%%%%%%%%%%%%% Module: Hydraulic System %%%%%%%%%%%%%% % The Hydraulic System (HS) is described by a directed graph G whose nodes % are tanks, jets, verniers, and pipe junctions, and whose arcs are labeled % by valves. The possible faults of the system on this level are leaky % valves, damaged jets, and valve stuck in one of their positions. % The purpose of this system is to prepare a set of jets for maneuvering % the shuttle in a certain direction. % % The HS representation of the struture of G is expressed by relation % link(N1,N2,V) representing the graph's connections. Setting the jets for % maneuvering the shuttle requires information about the jet's location in % the system (one of the four system's RCS) and the direction the % jet can fire. This is represented by the % following relations: jet_of(J,R) means that J is a jet of an rcs R, % direction(J,D) indicates that jet J fires in direction D, and % pair_of_jets(J1,J2) specifies which jets from the forward rcs must be % fired in pairs. We also need relations tank(X) and vernier(J) (the last % is not really used in this program, but will be needed later.) % % The initial state of the hydraulic system is characterized by the % values of the fluent in_state(V,S), read as valve V is in state S, % and a collection of faulty components described by atoms has_leak(V), % stuck(V) and damaged(J). It is assumed that all helium tanks are % pressurized at the initial state. % % The rules of HS define a function which takes the structural description % of HS and its initial state as an input and determines the distribution % of pressure from different tanks on the nodes of G, jets ready to fire, % and maneuvers ready to be performed. % % Each maneuver, maneuver(M), is described by a rule whose body can be % satisfied by a collection of jets located in the corresponding RCS's % and pointed in the specified directions. Performing a maneuver % corresponds to preparing such jets for firing. Fluent ready_to_fire(J) % is true when jet J is simultaneously pressurized by both fuel % and oxidizer tanks, and J is not damaged. A fluent pressurized_by(N,TK), % which reads node N is pressurized by tank TK, is true if there is an % open and non-leaking path from TK to N. To define such path we use % an auxiliary fluent leaking(N) where N is a node of graph G. %%%%%%%%%%%%%%%%%%%%%%% FACTS %%%%%%%%%%%%%%%%%%%%%%%% % link(N1,N2,V) is true iff node N1 is connected to node N2 via valve V. % links for fuel lines % Forward RCS link(ffh,ff,ffha). link(ffh,ff,ffhb). link(ff,ffj,ffdummy). link(ffj,ff12j,ffi12). link(ffj,ff345j,ffi345). link(ff12j,f1u,ffm1). link(ff12j,f1f,ffm1). link(ff12j,f1l,ffm1). link(ff12j,f1d,ffm1). link(ff12j,f2u,ffm2). link(ff12j,f2f,ffm2). link(ff12j,f2r,ffm2). link(ff12j,f2d,ffm2). link(ff345j,f3u,ffm3). link(ff345j,f3f,ffm3). link(ff345j,f3l,ffm3). link(ff345j,f3d,ffm3). link(ff345j,f4r,ffm4). link(ff345j,f4d,ffm4). link(ff345j,f5l,ffm5). link(ff345j,f5r,ffm5). % Left RCS link(lfh,lf,lfha). link(lfh,lf,lfhb). link(lf,lfj,lfdummy). link(lfj,lf12j,lfi12). link(lfj,lf345j,lfi345a). link(lfj,lf345j,lfi345b). link(lf12j,l1u,lfm1). link(lf12j,l1a,lfm1). link(lf12j,l1l,lfm1). link(lf12j,l2u,lfm2). link(lf12j,l2d,lfm2). link(lf12j,l2l,lfm2). link(lf12j,fxfeed,lfx12). link(fxfeed,lf12j,lfx12). link(lf345j,l3a,lfm3). link(lf345j,l3d,lfm3). link(lf345j,l3l,lfm3). link(lf345j,l4u,lfm4). link(lf345j,l4d,lfm4). link(lf345j,l4l,lfm4). link(lf345j,l5d,lfm5). link(lf345j,l5l,lfm5). link(lf345j,fxfeed,lfx345). link(fxfeed,lf345j,lfx345). % Right RCS link(rfh,rf,rfha). link(rfh,rf,rfhb). link(rf,rfj,rfdummy). link(rfj,rf12j,rfi12). link(rfj,rf345j,rfi345a). link(rfj,rf345j,rfi345b). link(rf12j,r1u,rfm1). link(rf12j,r1a,rfm1). link(rf12j,r1r,rfm1). link(rf12j,r2u,rfm2). link(rf12j,r2d,rfm2). link(rf12j,r2r,rfm2). link(rf12j,fxfeed,rfx12). link(fxfeed,rf12j,rfx12). link(rf345j,r3a,rfm3). link(rf345j,r3d,rfm3). link(rf345j,r3r,rfm3). link(rf345j,r4u,rfm4). link(rf345j,r4d,rfm4). link(rf345j,r4r,rfm4). link(rf345j,r5d,rfm5). link(rf345j,r5r,rfm5). link(rf345j,fxfeed,rfx345). link(fxfeed,rf345j,rfx345). % links for oxidizer lines % Forward RCS link(foh,fo,foha). link(foh,fo,fohb). link(fo,foj,fodummy). link(foj,fo12j,foi12). link(foj,fo345j,foi345). link(fo12j,f1u,fom1). link(fo12j,f1f,fom1). link(fo12j,f1l,fom1). link(fo12j,f1d,fom1). link(fo12j,f2u,fom2). link(fo12j,f2f,fom2). link(fo12j,f2r,fom2). link(fo12j,f2d,fom2). link(fo345j,f3u,fom3). link(fo345j,f3f,fom3). link(fo345j,f3l,fom3). link(fo345j,f3d,fom3). link(fo345j,f4r,fom4). link(fo345j,f4d,fom4). link(fo345j,f5l,fom5). link(fo345j,f5r,fom5). % Left RCS link(loh,lo,loha). link(loh,lo,lohb). link(lo,loj,lodummy). link(loj,lo12j,loi12). link(loj,lo345j,loi345a). link(loj,lo345j,loi345b). link(lo12j,l1u,lom1). link(lo12j,l1a,lom1). link(lo12j,l1l,lom1). link(lo12j,l2u,lom2). link(lo12j,l2d,lom2). link(lo12j,l2l,lom2). link(lo12j,oxfeed,lox12). link(oxfeed,lo12j,lox12). link(lo345j,l3a,lom3). link(lo345j,l3d,lom3). link(lo345j,l3l,lom3). link(lo345j,l4u,lom4). link(lo345j,l4d,lom4). link(lo345j,l4l,lom4). link(lo345j,l5d,lom5). link(lo345j,l5l,lom5). link(lo345j,oxfeed,lox345). link(oxfeed,lo345j,lox345). % Right RCS link(roh,ro,roha). link(roh,ro,rohb). link(ro,roj,rodummy). link(roj,ro12j,roi12). link(roj,ro345j,roi345a). link(roj,ro345j,roi345b). link(ro12j,r1u,rom1). link(ro12j,r1a,rom1). link(ro12j,r1r,rom1). link(ro12j,r2u,rom2). link(ro12j,r2d,rom2). link(ro12j,r2r,rom2). link(ro12j,oxfeed,rox12). link(oxfeed,ro12j,rox12). link(ro345j,r3a,rom3). link(ro345j,r3d,rom3). link(ro345j,r3r,rom3). link(ro345j,r4u,rom4). link(ro345j,r4d,rom4). link(ro345j,r4r,rom4). link(ro345j,r5d,rom5). link(ro345j,r5r,rom5). link(ro345j,oxfeed,rox345). link(oxfeed,ro345j,rox345). % The RCS system is divided into three subsystems expressed % by system(fwd_rcs). system(left_rcs). system(right_rcs). % tank_of(X,R) is true iff X is a tank of RCS R. tank_of(ffh,fwd_rcs). % ffh = forward fuel helium tank tank_of(ff,fwd_rcs). % ff = forward fuel propellant tank tank_of(foh,fwd_rcs). % foh = forward oxidizer helium tank tank_of(fo,fwd_rcs). % fo = forward oxidizer propellant tank tank_of(lfh,left_rcs). % lfh = left fuel helium tank. tank_of(lf,left_rcs). % lf = left fuel propellant tank. tank_of(loh,left_rcs). % loh = left oxidizer helium tank. tank_of(lo,left_rcs). % lo = left oxidizer propellant tank. tank_of(rfh,right_rcs). % rfh = right fuel helium tank. tank_of(rf,right_rcs). % rf = right fuel propellant tank. tank_of(roh,right_rcs). % roh = right oxidizer helium tank. tank_of(ro,right_rcs). % ro = right oxidizer propellant tank. tank_of(ohmsf,ohms). % ohmsf = ohms fuel propellant tank. tank_of(ohmso,ohms). % ohmso = ohms oxidizer propellant tank. % jet_of(J,R) is true iff J is a jet belonging to rcs R. jet_of(f1u,fwd_rcs). % f1u = forward_rcs 1 up jet_of(f1f,fwd_rcs). % f1f = forward_rcs 1 forward jet_of(f1l,fwd_rcs). % f1l = forward_rcs 1 left jet_of(f1d,fwd_rcs). % f1d = forward_rcs 1 down jet_of(f2u,fwd_rcs). % f2u = forward_rcs 2 up jet_of(f2f,fwd_rcs). % f2f = forward_rcs 2 forward jet_of(f2r,fwd_rcs). % f2r = forward_rcs 2 right jet_of(f2d,fwd_rcs). % f2d = forward_rcs 2 down jet_of(f3u,fwd_rcs). % f3u = forward_rcs 3 up jet_of(f3f,fwd_rcs). % f3f = forward_rcs 3 forward jet_of(f3l,fwd_rcs). % f3l = forward_rcs 3 left jet_of(f3d,fwd_rcs). % f3d = forward_rcs 3 down jet_of(f4r,fwd_rcs). % f4r = forward_rcs 4 right jet_of(f4d,fwd_rcs). % f4d = forward_rcs 4 down jet_of(l1u,left_rcs). % l1u = left_rcs 1 up jet_of(l1a,left_rcs). % l1f = left_rcs 1 aft jet_of(l1l,left_rcs). % l1l = left_rcs 1 left jet_of(l2u,left_rcs). % l2u = left_rcs 2 up jet_of(l2l,left_rcs). % l2f = left_rcs 2 left jet_of(l2d,left_rcs). % l2d = left_rcs 2 down jet_of(l3a,left_rcs). % l3u = left_rcs 3 aft jet_of(l3l,left_rcs). % l3l = left_rcs 3 left jet_of(l3d,left_rcs). % l3d = left_rcs 3 down jet_of(l4u,left_rcs). % l4d = left_rcs 4 up jet_of(l4l,left_rcs). % l4r = left_rcs 4 left jet_of(l4d,left_rcs). % l4d = left_rcs 4 down jet_of(r1u,right_rcs). % r1u = right_rcs 1 up jet_of(r1a,right_rcs). % r1f = right_rcs 1 aft jet_of(r1r,right_rcs). % r1l = right_rcs 1 right jet_of(r2u,right_rcs). % r2u = right_rcs 2 up jet_of(r2r,right_rcs). % r2f = right_rcs 2 right jet_of(r2d,right_rcs). % r2d = right_rcs 2 down jet_of(r3a,right_rcs). % r3u = right_rcs 3 aft jet_of(r3r,right_rcs). % r3l = right_rcs 3 right jet_of(r3d,right_rcs). % r3d = right_rcs 3 down jet_of(r4u,right_rcs). % r4d = right_rcs 4 up jet_of(r4r,right_rcs). % r4r = right_rcs 4 right jet_of(r4d,right_rcs). % r4d = right_rcs 4 down % verniers - small jets vernier_of(f5l,fwd_rcs). % f5l = forward_rcs 5 left vernier_of(f5r,fwd_rcs). % f5r = forward_rcs 5 right vernier_of(l5l,left_rcs). % l5l = left_rcs 5 left vernier_of(l5d,left_rcs). % l5d = left_rcs 5 down vernier_of(r5r,right_rcs). % r5r = right_rcs 5 right vernier_of(r5d,right_rcs). % r5d = right_rcs 5 down % direction(J,D) iff jet J fires in direction D. direction(f1f,forward). direction(f2f,forward). direction(f3f,forward). direction(f1u,up). direction(f2u,up). direction(f3u,up). direction(l1u,up). direction(l2u,up). direction(l4u,up). direction(r1u,up). direction(r2u,up). direction(r4u,up). direction(f1d,down). direction(f2d,down). direction(f3d,down). direction(f4d,down). direction(l2d,down). direction(l3d,down). direction(l4d,down). direction(r2d,down). direction(r3d,down). direction(r4d,down). direction(l1a,aft). direction(l3a,aft). direction(r1a,aft). direction(r3a,aft). direction(f1l,left). direction(f3l,left). direction(l1l,left). direction(l2l,left). direction(l3l,left). direction(l4l,left). direction(f2r,right). direction(f4r,right). direction(r1r,right). direction(r2r,right). direction(r3r,right). direction(r4r,right). % The downward firing jets on the forward rcs must be used % in pairs, one on each side. % pair_of_jets(J1,J2) is true iff jets J1 and J2 are a valid % pair of downward firing jets on the forward rcs. pair_of_jets(f1d,f2d). pair_of_jets(f1d,f4d). pair_of_jets(f3d,f2d). pair_of_jets(f3d,f4d). % The RCS system allows the space shuttle to perform the following % maneuvers: maneuver(minus_x). maneuver(plus_x). maneuver(minus_y). maneuver(plus_y). maneuver(minus_z). maneuver(plus_z). maneuver(minus_roll). maneuver(plus_roll). maneuver(minus_pitch). maneuver(plus_pitch). maneuver(minus_yaw). maneuver(plus_yaw). %%%%%%%%%%%%%%%%%%%%%%%% RULES %%%%%%%%%%%%%%%%%%%%%%%%% % A node is leaking at any time it is connected to a leaking valve % which is open. h(leaking(N1), T) :- time(T), link(N1,N2,V), has_leak(V), h(in_state(V,open),T). % A node is leaking if it is connected by an open valve to another node % which is leaking. h(leaking(N1),T) :- time(T), link(N1,N2,V), h(in_state(V,open),T), h(leaking(N2),T). % Non-tank node N1 is pressurized by tank X if it is not leaking and % is connected by an open valve to a node which is pressurized by tank X. h(pressurized_by(N1,X),T) :- time(T), not tank_of(N1,R), link(N2,N1,V), h(in_state(V,open),T), tank_of(X,R), h(pressurized_by(N2,X),T), not h(leaking(N1),T). % Tank node N1 is pressurized by tank X if it is connected % by an open valve to a node which is pressurized by tank X. h(pressurized_by(N1,X),T) :- time(T), tank_of(N1,R), link(N2,N1,V), h(in_state(V,open),T), tank_of(X,R), h(pressurized_by(N2,X),T). % The crossfeeds cannot be simultaneously pressurized by two tanks. :- time(T), tank_of(X,R), tank_of(Y,R1), neq(X,Y), h(pressurized_by(fxfeed,X),T), h(pressurized_by(fxfeed,Y),T). :- time(T), tank_of(X,R), tank_of(Y,R1), neq(X,Y), h(pressurized_by(oxfeed,X),T), h(pressurized_by(oxfeed,Y),T). % A jet is ready to fire iff it is pressurized by both fuel % and oxidizer tanks and it is not damaged. h(ready_to_fire(J),T) :- time(T), jet_of(J,R), tank_of(TK1,R1), %% marcy 05/12/2003 tank_of(TK2,R2), %% marcy 05/12/2003 neq(TK1,TK2), h(pressurized_by(J,TK1),T), h(pressurized_by(J,TK2),T), not damaged(J). % Do the same conditions of firing a jet apply to firing a vernier? % A vernier jet is ready to fire iff it is pressurized by both fuel % and oxidizer tanks and it is not damaged. h(fire_vernier(J),T) :- time(T), vernier_of(J,R), tank_of(TK1,R), tank_of(TK2,R), neq(TK1,TK2), h(pressurized_by(J,TK1),T), h(pressurized_by(J,TK2),T), not damaged(J). % The shuttle is ready for a maneuver X iff a set of jets % satisfying the requirements for maneuver X are ready to fire. % In order to increase the efficiency in planning the actions % required for a maneuver, we represent a maneuver X by its % three subparts each corresponding to the portion executed by % a different RCS subsystem % h(maneuver_of(X,S),T). % % If maneuver X does not involve any action of RCS subsystem S % we add atom "done(X,S)" to the description. The following rule % ensures that maneuver X of subsystem S is ready at time T. h(maneuver_of(X,S),T) :- time(T), done(X,S). % The shuttle is ready for maneuver +X if an aft jet is ready % to fire on both the left and right rcs. h(maneuver_of(plus_x,left_rcs),T) :- time(T), jet_of(J,left_rcs), direction(J,aft), h(ready_to_fire(J),T). h(maneuver_of(plus_x,right_rcs),T) :- time(T), jet_of(J,right_rcs), direction(J,aft), h(ready_to_fire(J),T). done(plus_x,fwd_rcs). % The shuttle is ready for maneuver -X if two of the forward % jets on the forward rcs are ready to fire. h(maneuver_of(minus_x,fwd_rcs),T) :- time(T), jet_of(J1,fwd_rcs), jet_of(J2,fwd_rcs), direction(J1,forward), direction(J2,forward), neq(J1,J2), h(ready_to_fire(J1),T), h(ready_to_fire(J2),T). done(minus_x,left_rcs). done(minus_x,right_rcs). % The shuttle is ready for maneuver +Y if a left jet is ready % to fire on both the left and forward rcs. h(maneuver_of(plus_y,left_rcs),T) :- time(T), jet_of(J,left_rcs), direction(J,left), h(ready_to_fire(J),T). h(maneuver_of(plus_y,fwd_rcs),T) :- time(T), jet_of(J,fwd_rcs), direction(J,left), h(ready_to_fire(J),T). done(plus_y,right_rcs). % The shuttle is ready for maneuver -Y if a right jet is ready % to fire on both the right and forward rcs. h(maneuver_of(minus_y,right_rcs),T) :- time(T), jet_of(J,right_rcs), direction(J,right), h(ready_to_fire(J),T). h(maneuver_of(minus_y,fwd_rcs),T) :- time(T), jet_of(J,fwd_rcs), direction(J,right), h(ready_to_fire(J),T). done(minus_y,left_rcs). % The shuttle is ready for maneuver +Z if an upward jet is ready % to fire on all three rcs'. h(maneuver_of(plus_z,left_rcs),T) :- time(T), jet_of(J,left_rcs), direction(J,up), h(ready_to_fire(J),T). h(maneuver_of(plus_z,right_rcs),T) :- time(T), jet_of(J,right_rcs), direction(J,up), h(ready_to_fire(J),T). h(maneuver_of(plus_z,fwd_rcs),T) :- time(T), jet_of(J,fwd_rcs), direction(J,up), h(ready_to_fire(J),T). % The shuttle is ready for maneuver -Z if a downward jet is % ready to fire on the right and left rcs, and a pair of % downward jets on the forward rcs. h(maneuver_of(minus_z,left_rcs),T) :- time(T), jet_of(J,left_rcs), direction(J,down), h(ready_to_fire(J),T). h(maneuver_of(minus_z,right_rcs),T) :- time(T), jet_of(J,right_rcs), direction(J,down), h(ready_to_fire(J),T). h(maneuver_of(minus_z,fwd_rcs),T) :- time(T), pair_of_jets(J1,J2), h(ready_to_fire(J1),T), h(ready_to_fire(J2),T). % The shuttle is ready for maneuver +roll if a downward jet on the % left rcs and an upward jet on the right rcs are both ready to fire. h(maneuver_of(plus_roll,left_rcs),T) :- time(T), jet_of(J,left_rcs), direction(J,down), h(ready_to_fire(J),T). h(maneuver_of(plus_roll,right_rcs),T) :- time(T), jet_of(J,right_rcs), direction(J,up), h(ready_to_fire(J),T). done(plus_roll,fwd_rcs). % The shuttle is ready for maneuver -roll if an upward jet on the % left rcs and a downward jet on the right rcs are both ready to fire. h(maneuver_of(minus_roll,left_rcs),T) :- time(T), jet_of(J,left_rcs), direction(J,up), h(ready_to_fire(J),T). h(maneuver_of(minus_roll,right_rcs),T) :- time(T), jet_of(J,right_rcs), direction(J,down), h(ready_to_fire(J),T). done(minus_roll,fwd_rcs). % The shuttle is ready for maneuver +pitch if a pair of downward % jets are ready to fire on the forward rcs and an upward jet is % ready to fire on the left and right rcs. h(maneuver_of(plus_pitch,fwd_rcs),T) :- time(T), pair_of_jets(J1,J2), h(ready_to_fire(J1),T), h(ready_to_fire(J2),T). h(maneuver_of(plus_pitch,left_rcs),T) :- time(T), jet_of(J,left_rcs), direction(J,up), h(ready_to_fire(J),T). h(maneuver_of(plus_pitch,right_rcs),T) :- time(T), jet_of(J,right_rcs), direction(J,up), h(ready_to_fire(J),T). % The shuttle is ready for maneuver -pitch if an upward jet is % ready to fire on the forward rcs and a downward jet is ready % to fire on the left and right rcs. h(maneuver_of(minus_pitch,fwd_rcs),T) :- time(T), jet_of(J,fwd_rcs), direction(J,up), h(ready_to_fire(J),T). h(maneuver_of(minus_pitch,left_rcs),T) :- time(T), jet_of(J,left_rcs), direction(J,down), h(ready_to_fire(J),T). h(maneuver_of(minus_pitch,right_rcs),T) :- time(T), jet_of(J,right_rcs), direction(J,down), h(ready_to_fire(J),T). % The shuttle is ready for maneuver +yaw if a right jet is ready % to fire on the right rcs and a left jet is ready to fire on the % forward rcs. h(maneuver_of(plus_yaw,right_rcs),T) :- time(T), jet_of(J,right_rcs), direction(J,right), h(ready_to_fire(J),T). h(maneuver_of(plus_yaw,fwd_rcs),T) :- time(T), jet_of(J,fwd_rcs), direction(J,left), h(ready_to_fire(J),T). done(plus_yaw,left_rcs). % The shuttle is ready for maneuver -yaw if a left jet is ready % to fire on the left rcs and a right jet is ready to fire on the % forward rcs. h(maneuver_of(minus_yaw,left_rcs),T) :- time(T), jet_of(J,left_rcs), direction(J,left), h(ready_to_fire(J),T). h(maneuver_of(minus_yaw,fwd_rcs),T) :- time(T), jet_of(J,fwd_rcs), direction(J,right), h(ready_to_fire(J),T). done(minus_yaw,right_rcs). %%%%%%%%%%%%%%%%%%%% Inertia Laws %%%%%%%%%%%%%%%%%%%%%%%% % Tanks mantain correct pressure unless some leak % occurs along their path for some time. h(pressurized_by(X,X),T1) :- next(T,T1), tank_of(X,R), h(pressurized_by(X,X),T), not nh(pressurized_by(X,X),T1). %% Question for Matt Barry: %% ??? delayed effect - instead of T1 some T+10 ???? %nh(pressurized_by(X,X),T1) :- next(T,T1), % tank_of(X,R), % link(X,N,V), % h(in_state(V,open),T), % h(leaking(N),T). %%%%%%%%%%%%%%%% Consistency constraints %%%%%%%%%%%%%%%%%% :- time(T), link(N2,N,V), tank_of(X,R), h(pressurized_by(N,X),T), nh(pressurized_by(N,X),T). :- time(T), link(N,N2,V), h(leaking(N),T), nh(leaking(N),T). %%%%%%%%%%%%% End of Module: Hydraulic System %%%%%%%%%%%%%% %%%%%%%%%%%%%%% Module: Valve Control System %%%%%%%%%%%%%% % % Valves of the RCS system can be opened and closed by manipulating % mechanical switches connected to them or by issuing computer commands. % Under normal circumstances, the on-board general purpose computer(s) % will be in charge of opening/closing valves and will achieve this % objective by sending computer commands. If the computer system is % malfunctioning an astronaut can normally override these commands by % manually flipping the switches that control the valves to be % opened/closed. Switches and computer commands are connected to % valves by electrical circuits. % % The VCS describes how computer commands and changes in the position % of switches affect the state of valves. The VCS has two levels of detail. % At the higher level, it is assumed that all electrical circuits are % working properly and therefore circuits are not included in the % representation. The lower level includes information about electrical % circuits of the system. It is normally used when some of the circuits % are malfunctioning, and therefore flipping the switches and issuing % the computer commands can produce results unexpected by the high-level % representation. % % % HIGH-LEVEL VALVE CONTROL SYSTEM % =============================== % % At this level, the VCS is described by a set of switches, computer % commands and valves, and by connections among them. Switches and valves % will be called "devices". % % Connections between switches and valves are described by the relation % % controls(Sw,V) % % meaning that switch Sw controls the state of valve V. Connections % between computer commands and valves are described by the relation % % commands(CC,V,S) % % meaning that computer command CC commands valve V to move to state S. % A malfunctioning of the circuitry controlling valve V is represented % by the relation % bad_circuitry(V) % % The fact that a device is malfunctioning is represented by the relation % % stuck(D,S) % % meaning that device D is stuck in state S. The rule stuck(D) :- stuck(D,S). % says that a device D is stuck if it is stuck in state S. % % Normally there is a set, C, of computer commands responsible for % moving a valve V into state S. There are two types of such sets, denoted % by "and" and "or". If C is of type "and" then V is moved to S only if all % the commands from C are issued simultaneously. Otherwise issuing one % command from C is sufficient to achieve the desired effect. Information % about the type of C is recorded by the statement % % command_type(V,S,Ty) % % meaning that the set of computer commands responsible for moving valve V % into state S is of type Ty. % % % The dynamic behaviour of the high-level VCS is described by a set of fluents % and actions. Actions are represented as follows: % % action(flip(D,S)) - flips switch D to state S % action(cc(V,S)) - issue all the computer commands required to move % valve V to state S % action(CC) - issues computer command CC. % % The state of a device is described by the fluent % % in_state(D,S) % % meaning that device D is in state S. % Normally computer commands are issued to a valve only when the switch % connected to the valve is in gpc state. If a computer command is issued % when the switch is not in gpc state, the state of the valve is undefined % in the high-level VCS and the input is considered abnormal. % This is represented by the fluent % % ab_input(V) % % The input of high-level VCS consists of: % 1) a collection of statements of the form h(is_state(D,S),0) describing % the states of switches and valves in the initial situation; % 2) the description of possible malfunctionings of switches and valves; % 3) the sequence of actions which defines the past history of events up to % moment T. % Notice that fluents of the form ab_input(V) cannot be part of the description % of the initial situation and this is enforced by the constraint: :- controls(Sw,V), h(ab_input(V),0). % The output of this module is a description of the state of valves and % switches at time T+1. % % % The effects of actions are defined by the following dynamic causal laws. % % If a properly working switch Sw is flipped to state S at time T, then % Sw will be in state S at the next moment of time. h(in_state(Sw,S),T1) :- next(T,T1), of_type(Sw,v_switch), state_of(S,v_switch), occurs(flip(Sw,S),T), not stuck(Sw). % If the switch controlling valve V is in gpc state, V is working % properly, and all the computer commands required to move V to some state S % were issued at time T, then V is in state S at the next moment of time. h(in_state(V,S),T1) :- next(T,T1), controls(Sw,V), h(in_state(Sw,gpc),T), occurs(CC,T), commands(CC,V,S), not stuck(V), not bad_circuitry(V). % Note: we need to consider the case when two opposite cc's are issued. % In this case, the basic level can not determine the state of the valve, % instead the extended level should be used. % For that, we need to include condition: not ab_input(V) to the above % rule, and add a new rule with h(ab_input(V),T) as head saying that it is % abnormal if two opposite cc's are issued simultaneously at T. % A static connection between switches and valves is expressed by a % static law. % % If switch Sw controlling a valve V is in some state S (open or closed) % at time T, and both V and its connection to Sw are working properly, and % the input is not abnormal, then V is also in state S at the same time. h(in_state(V,S),T) :- time(T), controls(Sw,V), h(in_state(Sw,S),T), state_of(S,v_switch), neq(S,gpc), not h(ab_input(V),T), not stuck(V), not bad_circuitry(V). % If switch Sw controlling a valve V is in some state S (open or closed) % at time T, and all computer command required to move V to some state P % (different from S) were issued at time T, then the input to V is considered % abnormal at time T+1, i.e. the state of V is undefined in high-level VCS. h(ab_input(V),T1) :- next(T,T1), controls(Sw,V), h(in_state(Sw,S),T), occurs(CC,T), commands(CC,V,P), state_of(S,v_switch), neq(S,gpc), neq(S,P), not bad_circuitry(V). % A device is always on a state S if it stuck at S. h(in_state(D,S),0) :- stuck(D,S). %%%%%%%%%%%%%%%%%%%%%%% FACTS %%%%%%%%%%%%%%%%%%%%%%%% % state_of(S,D) is true iff S is the state of device D. state_of(open, v_switch). state_of(closed, v_switch). state_of(gpc, v_switch). state_of(open,valve). state_of(closed,valve). opposite_state(open,closed). opposite_state(closed,open). % of_type(D,Dev) is true iff D is a device of type Dev. of_type(V,valve) :- controls(D,V). of_type(D,v_switch) :- controls(D,V). of_type(V,valve) :- dummy_valve(V). % Dummy valves have been added between fuel/oxidizer tanks % and the following junction node in order to correctly % determine when the junction node is leaking. dummy_valve(ffdummy). dummy_valve(fodummy). dummy_valve(lfdummy). dummy_valve(lodummy). dummy_valve(rfdummy). dummy_valve(rodummy). % controls(D,V) is true iff switch D controls valve V. % Each switch controls simultaneously two different valves. controls(D,V) :- controls(D,V,C). % controls(D,V,C) is true iff switch D controls valve V % via electrical circuit C. % Forward RCS controls(fha,ffha,fhca). controls(fha,foha,fhca). controls(fhb,ffhb,fhcb). controls(fhb,fohb,fhcb). controls(fi12,ffi12,fic12). controls(fi12,foi12,fic12). controls(fi345,ffi345,fic345). controls(fi345,foi345,fic345). controls(fm1,ffm1,fmc1). controls(fm1,fom1,fmc1). controls(fm2,ffm2,fmc2). controls(fm2,fom2,fmc2). controls(fm3,ffm3,fmc3). controls(fm3,fom3,fmc3). controls(fm4,ffm4,fmc4). controls(fm4,fom4,fmc4). controls(fm5,ffm5,fmc5). controls(fm5,fom5,fmc5). % Left RCS controls(lha,lfha,lhca). controls(lha,loha,lhca). controls(lhb,lfhb,lhcb). controls(lhb,lohb,lhcb). controls(li12,lfi12,lic12). controls(li12,loi12,lic12). controls(li345a,lfi345a,lic345a). controls(li345a,loi345a,lic345a). controls(li345b,lfi345b,lic345b). controls(li345b,loi345b,lic345b). controls(lm1,lfm1,lmc1). controls(lm1,lom1,lmc1). controls(lm2,lfm2,lmc2). controls(lm2,lom2,lmc2). controls(lm3,lfm3,lmc3). controls(lm3,lom3,lmc3). controls(lm4,lfm4,lmc4). controls(lm4,lom4,lmc4). controls(lm5,lfm5,lmc5). controls(lm5,lom5,lmc5). controls(lx12,lfx12,lxc12). controls(lx12,lox12,lxc12). controls(lx345,lfx345,lxc345). controls(lx345,lox345,lxc345). % Right RCS controls(rha,rfha,rhca). controls(rha,roha,rhca). controls(rhb,rfhb,rhcb). controls(rhb,rohb,rhcb). controls(ri12,rfi12,ric12). controls(ri12,roi12,ric12). controls(ri345a,rfi345a,ric345a). controls(ri345a,roi345a,ric345a). controls(ri345b,rfi345b,ric345b). controls(ri345b,roi345b,ric345b). controls(rm1,rfm1,rmc1). controls(rm1,rom1,rmc1). controls(rm2,rfm2,rmc2). controls(rm2,rom2,rmc2). controls(rm3,rfm3,rmc3). controls(rm3,rom3,rmc3). controls(rm4,rfm4,rmc4). controls(rm4,rom4,rmc4). controls(rm5,rfm5,rmc5). controls(rm5,rom5,rmc5). controls(rx12,rfx12,rxc12). controls(rx12,rox12,rxc12). controls(rx345,rfx345,rxc345). controls(rx345,rox345,rxc345). % basic_command(CC,V,S) is true iff a single computer command CC % moves valve V to state S. % Forward RCS % Commands to control valves ffha, ffhb, foha, fohb basic_command(opena_ffha,ffha,open). basic_command(opena_ffha,foha,open). basic_command(closea_ffha,ffha,closed). basic_command(closea_ffha,foha,closed). basic_command(opena_ffhb,ffhb,open). basic_command(opena_ffhb,fohb,open). basic_command(closea_ffhb,ffhb,closed). basic_command(closea_ffhb,fohb,closed). % Commands to control valves ffi12, foi12 basic_command(opena_ffi12,ffi12,open). basic_command(opena_foi12,foi12,open). % Commands to control valves ffi345, foi345 basic_command(opena_ffi345,ffi345,open). basic_command(opena_foi345,foi345,open). % Commands to control valves (manifolds) ffm1, fom1 basic_command(open_ffm1,ffm1,open). basic_command(open_ffm1,fom1,open). basic_command(closea_ffm1,ffm1,closed). basic_command(closea_ffm1,fom1,closed). basic_command(closeb_ffm1,ffm1,closed). basic_command(closeb_ffm1,fom1,closed). % Commands to control valves (manifolds) ffm2, fom2 basic_command(open_ffm2,ffm2,open). basic_command(open_ffm2,fom2,open). basic_command(closea_ffm2,ffm2,closed). basic_command(closea_ffm2,fom2,closed). basic_command(closeb_ffm2,ffm2,closed). basic_command(closeb_ffm2,fom2,closed). % Commands to control valves (manifolds) ffm3, fom3 basic_command(open_ffm3,ffm3,open). basic_command(open_ffm3,fom3,open). basic_command(closea_ffm3,ffm3,closed). basic_command(closea_ffm3,fom3,closed). basic_command(closeb_ffm3,ffm3,closed). basic_command(closeb_ffm3,fom3,closed). % Commands to control valves (manifolds) ffm4, fom4 basic_command(open_ffm4,ffm4,open). basic_command(open_ffm4,fom4,open). basic_command(closea_ffm4,ffm4,closed). basic_command(closea_ffm4,fom4,closed). basic_command(closeb_ffm4,ffm4,closed). basic_command(closeb_ffm4,fom4,closed). % Left RCS % Commands to control valves lfha, lohb, lfha, lohb basic_command(opena_lfha,lfha,open). basic_command(opena_lfha,loha,open). basic_command(closea_lfha,lfha,closed). basic_command(closea_lfha,loha,closed). basic_command(opena_lfhb,lfhb,open). basic_command(opena_lfhb,lohb,open). basic_command(closea_lfhb,lfhb,closed). basic_command(closea_lfhb,lohb,closed). % Commands to control valves lfi12, loi12 basic_command(opena_li12,lfi12,open). basic_command(opena_li12,loi12,open). basic_command(openb_lfi12,lfi12,open). basic_command(openb_loi12,loi12,open). % Commands to control valves (crossfeeds) lfx12, lox12 basic_command(opena_lx12,lfx12,open). basic_command(opena_lx12,lox12,open). basic_command(openb_lfx12,lfx12,open). basic_command(openb_lox12,lox12,open). % Commands to control valves lfi345a, lfi345b, loi345a, lfi345b basic_command(open_lfi345a,lfi345a,open). basic_command(open_loi345a,loi345a,open). basic_command(close_lfi345a,lfi345a,closed). basic_command(close_loi345a,loi345a,closed). basic_command(open_lfi345b,lfi345b,open). basic_command(open_loi345b,loi345b,open). basic_command(close_lfi345b,lfi345b,closed). basic_command(close_loi345b,loi345b,closed). % Commands to control valves (crossfeeds) lfx345, lox345 basic_command(open_lfx345,lfx345,open). basic_command(open_lox345,lox345,open). basic_command(close_lfx345,lfx345,closed). basic_command(close_lox345,lox345,closed). % Commands to control valves (manifolds) lfm1, lom1 basic_command(open_lfm1,lfm1,open). basic_command(open_lfm1,lom1,open). basic_command(closea_lfm1,lfm1,closed). basic_command(closea_lfm1,lom1,closed). basic_command(closeb_lfm1,lfm1,closed). basic_command(closeb_lfm1,lom1,closed). % Commands to control valves (manifolds) lfm2, lom2 basic_command(open_lfm2,lfm2,open). basic_command(open_lfm2,lom2,open). basic_command(closea_lfm2,lfm2,closed). basic_command(closea_lfm2,lom2,closed). basic_command(closeb_lfm2,lfm2,closed). basic_command(closeb_lfm2,lom2,closed). % Commands to control valves (manifolds) lfm3, lom3 basic_command(open_lfm3,lfm3,open). basic_command(open_lfm3,lom3,open). basic_command(closea_lfm3,lfm3,closed). basic_command(closea_lfm3,lom3,closed). basic_command(closeb_lfm3,lfm3,closed). basic_command(closeb_lfm3,lom3,closed). % Commands to control valves (manifolds) lfm4, lom4 basic_command(open_lfm4,lfm4,open). basic_command(open_lfm4,lom4,open). basic_command(closea_lfm4,lfm4,closed). basic_command(closea_lfm4,lom4,closed). basic_command(closeb_lfm4,lfm4,closed). basic_command(closeb_lfm4,lom4,closed). % Right RCS % Commands to control valves rfha, rohb, rfha, rohb basic_command(opena_rfha,rfha,open). basic_command(opena_rfha,roha,open). basic_command(closea_rfha,rfha,closed). basic_command(closea_rfha,roha,closed). basic_command(opena_rfhb,rfhb,open). basic_command(opena_rfhb,rohb,open). basic_command(closea_rfhb,rfhb,closed). basic_command(closea_rfhb,rohb,closed). % Commands to control valves rfi12, roi12 basic_command(opena_ri12,rfi12,open). basic_command(opena_ri12,roi12,open). basic_command(openb_rfi12,rfi12,open). basic_command(openb_roi12,roi12,open). % Commands to control valves (crossfeeds) rfx12, rox12 basic_command(opena_rx12,rfx12,open). basic_command(opena_rx12,rox12,open). basic_command(openb_rfx12,rfx12,open). basic_command(openb_rox12,rox12,open). % Commands to control valves rfi345a, rfi345b, roi345a, fi345b basic_command(open_rfi345a,rfi345a,open). basic_command(open_roi345a,roi345a,open). basic_command(close_rfi345a,rfi345a,closed). basic_command(close_roi345a,roi345a,closed). basic_command(open_rfi345b,rfi345b,open). basic_command(open_roi345b,roi345b,open). basic_command(close_rfi345b,rfi345b,closed). basic_command(close_roi345b,roi345b,closed). % Commands to control valves (crossfeeds) rfx345, rox345 basic_command(open_rfx345,rfx345,open). basic_command(open_rox345,rox345,open). basic_command(close_rfx345,rfx345,closed). basic_command(close_rox345,rox345,closed). % Commands to control valves (manifolds) rfm1, rom1 basic_command(open_rfm1,rfm1,open). basic_command(open_rfm1,rom1,open). basic_command(closea_rfm1,rfm1,closed). basic_command(closea_rfm1,rom1,closed). basic_command(closeb_rfm1,rfm1,closed). basic_command(closeb_rfm1,rom1,closed). % Commands to control valves (manifolds) rfm2, rom2 basic_command(open_rfm2,rfm2,open). basic_command(open_rfm2,rom2,open). basic_command(closea_rfm2,rfm2,closed). basic_command(closea_rfm2,rom2,closed). basic_command(closeb_rfm2,rfm2,closed). basic_command(closeb_rfm2,rom2,closed). % Commands to control valves (manifolds) rfm3, rom3 basic_command(open_rfm3,rfm3,open). basic_command(open_rfm3,rom3,open). basic_command(closea_rfm3,rfm3,closed). basic_command(closea_rfm3,rom3,closed). basic_command(closeb_rfm3,rfm3,closed). basic_command(closeb_rfm3,rom3,closed). % Commands to control valves (manifolds) rfm4, rom4 basic_command(open_rfm4,rfm4,open). basic_command(open_rfm4,rom4,open). basic_command(closea_rfm4,rfm4,closed). basic_command(closea_rfm4,rom4,closed). basic_command(closeb_rfm4,rfm4,closed). basic_command(closeb_rfm4,rom4,closed). % commands(CC,V,S) is true iff computer command CC moves % valve V to state S. commands(CC,V,S) :- basic_command(CC,V,S). % commands(cc(CC1,CC2),V,S) is true iff both computer commands % CC1 and CC2 must be issued to move % valve V to state S. % Forward RCS commands(cc(closea_fi12,closeb_ffi12),ffi12,closed). commands(cc(closea_fi12,closeb_foi12),foi12,closed). commands(cc(opena_ffm5,openb_ffm5),ffm5,open). commands(cc(opena_ffm5,openb_ffm5),fom5,open). commands(cc(closea_ffm5,closeb_ffm5),ffm5,closed). commands(cc(closea_ffm5,closeb_ffm5),fom5,closed). %% Question for Matt: should openc be or with closec??? %commands(openc_ffm5,ffm5,open). %commands(openc_ffm5,fom5,open). %commands(closec_ffm5,ffm5,closed). %commands(closec_ffm5,fom5,closed). % Left RCS commands(cc(closea_li12,closeb_lfi12),lfi12,closed). commands(cc(closea_li12,closeb_loi12),loi12,closed). commands(cc(close_lx12,close_lfx12),lfx12,closed). commands(cc(close_lx12,close_lox12),lox12,closed). commands(cc(opena_lfm5,openb_lfm5),lfm5,open). commands(cc(opena_lfm5,openb_lfm5),lom5,open). commands(cc(closea_lfm5,closeb_lfm5),lfm5,closed). commands(cc(closea_lfm5,closeb_lfm5),lom5,closed). %% Question for Matt: should openc be or with closec??? %commands(openc_lfm5,lfm5,open). %commands(openc_lfm5,lom5,open). %commands(closec_lfm5,lfm5,closed). %commands(closec_lfm5,lom5,closed). % Right RCS commands(cc(closea_ri12,closeb_rfi12),rfi12,closed). commands(cc(closea_ri12,closeb_roi12),roi12,closed). commands(cc(close_rx12,close_rfx12),rfx12,closed). commands(cc(close_rx12,close_rox12),rox12,closed). commands(cc(opena_rfm5,openb_rfm5),rfm5,open). commands(cc(opena_rfm5,openb_rfm5),rom5,open). commands(cc(closea_rfm5,closeb_rfm5),rfm5,closed). commands(cc(closea_rfm5,closeb_rfm5),rom5,closed). %% Question for Matt: should openc be or with closec??? %commands(openc_rfm5,rfm5,open). %commands(openc_rfm5,rom5,open). %commands(closec_rfm5,rfm5,closed). %commands(closec_rfm5,rom5,closed). %%%% Commands to open xfeed valves??? %%%%%%%%%%%%%%%%% Impossibility conditions %%%%%%%%%%%%%%%%% % A switch cannot be moved to a state it is already in. :- time(T), of_type(Sw,v_switch), state_of(S,v_switch), h(in_state(Sw,S),T), occurs(flip(Sw,S),T). %%%%%%%%%%%%%%%%%%%% Inertia Law %%%%%%%%%%%%%%%%%%%%%%%% % The inertia law expresses the following default law: % "Normally, things tend to stay as they were." h(in_state(D,S),T1) :- next(T,T1), of_type(D,Dev), state_of(S,Dev), h(in_state(D,S),T), not nh(in_state(D,S),T1). nh(in_state(D,S),T) :- time(T), of_type(D,Dev), state_of(S,Dev), state_of(S1,Dev), neq(S,S1), h(in_state(D,S1),T). %%%%%%%%%%%%%%%% Consistency constraints %%%%%%%%%%%%%%%%%% % A device can only be in one state at a time. :- time(T), of_type(D,Dev), state_of(S,Dev), h(in_state(D,S),T), nh(in_state(D,S),T). %%%%%%%%%%% End of Module: Valve Control System %%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%% Time %%%%%%%%%%%%%%%%%%%%%%%%% % The time range allowed for computation covers from moment 0 to % the moment defined by constant "lasttime," which is provided % by the user at run time. time(0..lasttime). % next(T,T1) is true iff the next moment of time after T is T1. next(T,T1) :- time(T), time(T1), T1=T+1. %%%%%%%%%%%%%%%%%% For Display Purposes %%%%%%%%%%%%%%%%%%% hide link(X,Y,Z). hide tank_of(X,Y). hide jet_of(X,Y). hide vernier_of(X,Y). hide direction(X,Y). hide pair_of_jets(X,Y). hide v_switch(X). hide has_leak(X). hide time(X). hide next(X,Y). hide nh(X,Y). hide h(X,Y). hide action(X). hide target_device(X,Y). hide target_state(X,Y). hide state_of(X,Y). hide of_type(X,Y). hide controls(X,Y,Z). hide controls(X,Y). hide commands(X,Y,Z). hide basic_command(X,Y,Z). hide type_of_valve(X,Y). hide input_of_type(X,Y). hide output_of_type(X,Y). hide elec_circ(C). hide connects(X,Y,W,Z). hide affected_by_switch(X,Y). hide stuck(X). hide stuck(X,Y). %hide occurs(X,Y). hide noccurs(X,Y). hide command_type(X,Y,Z). hide some_cc_not_issued(X,Y,Z). hide dummy_valve(X). hide opposite_state(X,Y). hide bad_circuitry(X). hide v_solenoid(X). hide done(X,Y). hide goal(X,Y). hide system(X). hide maneuver(X). hide goal. hide done(X). hide happened_before(X,Y).