% File: rcs2 % $Name: $ % %---------------------------------------------------------------------- % RCS VALVE CONTROL SYSTEM - LOW LEVEL %---------------------------------------------------------------------- bad_circuitry(V) :- elec_circ(C), controls(Sw,V,C). %bad_circuitry(V) :- elec_circ(C), % commands(CC,V,S,C). %%%%%%%%%%%%%%%%%% Module: SWITCHES %%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%% RULES %%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Normal behavior of switches on this level is described by the % following rules: % If switch D is in state S and value X is present on input Wi % (which corresponds to S) at time T, then the output Wo paired % with Wi will also have value X at time T. h(value(Wo,X),T) :- time(T), signal(X), connects(S,D,Wi,Wo), h(in_state(D,S),T), h(value(Wi,X),T), not bad_connections_in(D). % If switch D is in state S at time T, then output wires of all % pairs corresponding to states different from S will have value 0 % at time T. h(value(Wo,0),T) :- time(T), state_of(S,v_switch), h(in_state(D,S),T), connects(S1,D,Wi,Wo), neq(S,S1). % Bad connections in a device are expressed by %bad_connections_in(D) :- of_type(D,Dev), % state_of(S,Dev), % stuck(D,S). %%%%%%%%%%%%%%%%%% End of Module: SWITCHES %%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%% Module: VALVES %%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%% FACTS %%%%%%%%%%%%%%%%%%%%%%%%%%%%% % type_of_valve(V,Y) is true iff type of valve V is Y. % Forward RCS type_of_valve(ffha,solenoid). % have 2 input wires: open & close type_of_valve(foha,solenoid). type_of_valve(ffhb,solenoid). type_of_valve(fohb,solenoid). type_of_valve(ffi12,motor3). % have 3 input wires: open, closea & closeb type_of_valve(foi12,motor3). type_of_valve(ffi345,motor3). type_of_valve(foi345,motor3). type_of_valve(ffm1,motor2). % have 2 input wires: open & close type_of_valve(fom1,motor2). type_of_valve(ffm2,motor2). type_of_valve(fom2,motor2). type_of_valve(ffm3,motor2). type_of_valve(fom3,motor2). type_of_valve(ffm4,motor2). type_of_valve(fom4,motor2). type_of_valve(ffm5,solenoid). % have 2 input wires: open & close type_of_valve(fom5,solenoid). % Left RCS type_of_valve(lfha,solenoid). % have 2 input wires: open & close type_of_valve(loha,solenoid). type_of_valve(lfhb,solenoid). type_of_valve(lohb,solenoid). type_of_valve(lfi12,motor4). % have 4 inputs: opena,openb,closea & closeb type_of_valve(loi12,motor4). type_of_valve(lfi345a,motor2). % have 2 input wires: open & close type_of_valve(loi345a,motor2). type_of_valve(lfi345b,motor2). type_of_valve(loi345b,motor2). type_of_valve(lfm1,motor2). % have 2 input wires: open & close type_of_valve(lom1,motor2). type_of_valve(lfm2,motor2). type_of_valve(lom2,motor2). type_of_valve(lfm3,motor2). type_of_valve(lom3,motor2). type_of_valve(lfm4,motor2). type_of_valve(lom4,motor2). type_of_valve(lfm5,solenoid). % have 2 input wires: open & close type_of_valve(lom5,solenoid). type_of_valve(lfx12,motor4). % have 4 inputs: opena,openb,closea & closeb type_of_valve(lox12,motor4). type_of_valve(lfx345,motor4). type_of_valve(lox345,motor4). % Right RCS type_of_valve(rfha,solenoid). % have 2 input wires: open & close type_of_valve(roha,solenoid). type_of_valve(rfhb,solenoid). type_of_valve(rohb,solenoid). type_of_valve(rfi12,motor4). % have 4 inputs: opena,openb,closea & closeb type_of_valve(roi12,motor4). type_of_valve(rfi345a,motor2). % have 2 input wires: open & close type_of_valve(roi345a,motor2). type_of_valve(rfi345b,motor2). type_of_valve(roi345b,motor2). type_of_valve(rfm1,motor2). % have 2 input wires: open & close type_of_valve(rom1,motor2). type_of_valve(rfm2,motor2). type_of_valve(rom2,motor2). type_of_valve(rfm3,motor2). type_of_valve(rom3,motor2). type_of_valve(rfm4,motor2). type_of_valve(rom4,motor2). type_of_valve(rfm5,solenoid). % have 2 input wires: open & close type_of_valve(rom5,solenoid). type_of_valve(rfx12,motor4). % have 4 inputs: opena,openb,closea & closeb type_of_valve(rox12,motor4). type_of_valve(rfx345,motor4). type_of_valve(rox345,motor4). %%%%%%%%%%%%%%%%%%%%%%%%%%% RULES %%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Solenoid controlled valves (and also type "Motor2" valves) have two input % wires which correspond to OPEN or CLOSE valve operations, and an additional % input for power supply. % The state of a solenoid valve is determined on this level of abstraction % by rule % CHANGED BY MARCELLO (09/27/00) % Added neq(S,power_bus) and neq(S1,power_bus), in order to prevent the % valve from moving to state "power_bus". % h(in_state(V,S),T) :- time(T), v_solenoid(V), input(W1,V), input_of_type(W1,S), neq(S,power_bus), h(value(W1,1),T), input(W2,V), input_of_type(W2,S1), neq(S1,power_bus), h(value(W2,0),T), neq(S,S1), not stuck(V,S1). v_solenoid(V) :- type_of_valve(V,solenoid). v_solenoid(V) :- type_of_valve(V,motor2). % Motor controlled valves type "motor3" differ from solenoid controlled % valves in that the former have input wires corresponding to: OPEN, % CLOSE-A and CLOSE-B, plus an additional input reserved for connection to a % power bus source. However, motor controlled valves also have two output % wires for OPEN and CLOSE states as the solenoid controlled valves. % % There are only two combinations of inputs that will appropriately % activated the motor that controls the valve: % a. to close the valve the value of its input OPEN must be 0, and both % CLOSE-A and CLOSE-B inputs must be 1; % b. to open the valve the value of its input OPEN must be 1, and the % value of input CLOSE-B must be 0. % All other combinations of input values will not start the motor. % % The rules that represent the two operational conditions for opening/ % closing a motor controlled valve type "motor3" are h(in_state(V,closed),T) :- time(T), type_of_valve(V,motor3), input(W1,V), input_of_type(W1,open), h(value(W1,0),T), input(W2,V), input_of_type(W2,closea), h(value(W2,1),T), input(W3,V), input_of_type(W3,closeb), h(value(W3,1),T), not stuck(V,open). h(in_state(V,open),T) :- time(T), type_of_valve(V,motor3), input(W1,V), input_of_type(W1,open), h(value(W1,1),T), input(W2,V), input_of_type(W2,closeb), h(value(W2,0),T), not stuck(V,closed). % For motor controlled valve type "motor4" we have % Valve closes if both closea and closeb inputs are 1 and both % opena and openb inputs are 0. h(in_state(V,closed),T) :- time(T), type_of_valve(V,motor4), input(W1,V), input_of_type(W1,opena), h(value(W1,0),T), input(W2,V), input_of_type(W2,openb), h(value(W2,0),T), input(W3,V), input_of_type(W3,closea), h(value(W3,1),T), input(W4,V), input_of_type(W4,closeb), h(value(W4,1),T), not stuck(V,open). % If at least one of the open inputs is 1 then valve opens. h(in_state(V,open),T) :- time(T), type_of_valve(V,motor4), input(W1,V), input_of_type(W1,opena), h(value(W1,1),T), not stuck(V,closed). h(in_state(V,open),T) :- time(T), type_of_valve(V,motor4), input(W1,V), input_of_type(W1,openb), h(value(W1,1),T), not stuck(V,closed). % Values on output wires of both solenoid and motor controlled valves % are determined by rules: % If valve V is in state S at time T, then the value on the % output wire (corresponding to S) of V is 1 at T when V is powered. % % changed by marcy (10/18/02) % % until we further investigate the subject, we will % not distinguish between the time taken by a solenoid % valve to generate its output and the time taken by % a non-solenoid valve. % h(value(W,1),T) :- time(T), of_type(V,valve), % type_of_valve(V,solenoid), h(in_state(V,S),T), output(W,V), output_of_type(W,S), input(Wp,V), input_of_type(Wp,power_bus), h(value(Wp,1),T). %h(value(W,1),T1) :- next(T,T1), % of_type(V,valve), % not type_of_valve(V,solenoid), % h(in_state(V,S),T), % output(W,V), % output_of_type(W,S), % input(Wp,V), % input_of_type(Wp,power_bus), % h(value(Wp,1),T). %%%% ATTENTION: be sure that we have power buses connected to valves %%%% no control buses. % Values on ouput wires of a valve V indicate the state of V, and % are therefore multually exclusive under normal behavior. If an % output wire has a value 1 at time T, then the value on the other % output wire is 0 at T. h(value(W2,0),T) :- time(T), of_type(V,valve), output(W1,V), output(W2,V), neq(W1,W2), h(value(W1,1),T). % If a valve has no power (abnormal condition) then all its output % wires have value 0. h(value(W,0),T) :- time(T), of_type(V,valve), output(W,V), input(Wp,V), input_of_type(Wp,power_bus), h(value(Wp,0),T). %%%% ATTENTION: be sure that we have power buses connected to valves %%%% no control buses. %%%%%%%%%%%%%%%%%% End of Module: VALVES %%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%% Module: POWER BUS %%%%%%%%%%%%%%%%% % Different power buses of both d.... (dc) and alternating current (ac) % provide electrical power to the RCS to allow the operation of switches, % valves, and other devices. These diverse sources of energy will be % represent by power buses activated through manual on/off switches. ??????? %%%%%%%%%%%%%%%%%%%%%%%%%%% RULES %%%%%%%%%%%%%%%%%%%%%%%%%%%% % % For simplicity, a power bus will be modeled as a device with no inputs % and a single output which is always 1 under normal functioning conditions. % If the power bus is faulty its output will have value 0. h(value(W,1),T) :- time(T), of_type(D,power_bus), output(W,D), not bad_device(D). h(value(W,0),T) :- time(T), of_type(D,power_bus), output(W,D), bad_device(D). %%%%%%%%%%%%%%%%%% End of Module: POWER BUS %%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%% Module: CONTROL BUS %%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%% RULES %%%%%%%%%%%%%%%%%%%%%%%%%%%% % % For simplicity, a control bus will be modeled as a device with no inputs % and a single output which is always 1 under normal functioning conditions. % If the control bus is faulty its output will have value 0. h(value(W,1),T) :- time(T), of_type(D,control_bus), output(W,D), not bad_device(D). h(value(W,0),T) :- time(T), of_type(D,control_bus), output(W,D), bad_device(D). %%%%%%%%%%%%%%%%%% End of Module: CONTROL BUS %%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%% Module: COMPUTER COMMAND %%%%%%%%%%%%%%%%% % The space shuttle flight computer software is contained in its five % general purpose computers (GPCs) which control the vehicle. The data % processing system (DPS) allows control of all RCS activity being % responsible for transmiting commands for valve configuration and jet % firings. % If a switch is placed in GPC state, computer commands can be output % to open or close the affected valves. % Issuing a computer command is represented as an action that will % affect a target device D by setting D to a new state. %%%%%%%%%%%%%%%%%%%%%%%%%%% RULES %%%%%%%%%%%%%%%%%%%%%%%%%%%% % Issuing a computer command CC is expressed on this level by applying % a value of 1 on the wire connecting CC to a gate in the circuit. h(value(W,1),T1) :- next(T,T1), % marcy (10/18/02) -- for consistency with the way time flows during flip actions % time(T), commands(CC,V,S), output(W,CC), % occurs(cc(V,S),T). occurs(CC,T). % modified by marcy (10/18/02) -- CC's do not have the cc(V,S) form in the Extended VCM % On the absence of computer commands, a signal of value 0 % should be present on the wires that connect some device of % an electrical circuit to the computers. h(value(W,0),T) :- time(T), commands(CC,V,S), output(W,CC), not h(value(W,1),T). %%%%%%%%%%%%%%% End of Module: COMPUTER COMMAND %%%%%%%%%%%%%%