TYPES
generator: Source(AC);
AC bus: Bus(AC);
DC bus: Bus(DC);
rectifier: Converter(AC, DC);
load: Sink(DC);
contactor: Switch;


COMPONENTS
left generator: 1;
right generator: 1;
left AC bus: 1;
right AC bus: 1;
left rectifier: 1;
right rectifier: 1;
left DC bus: 1;
right DC bus: 1;
left load: 1;
right load: 1;
contactor: *;

ABBREVIATIONS
left generator 1: LG1;
right generator 1: RG1;
left AC bus 1: LB1;
right AC bus 1: RB1;
left rectifier 1: LR1;
right rectifier 1: RR1;
right DC bus 1: RD1;
left DC bus 1: LD1;
left load 1: LL1;
right load 1: RL1;

CONNECTIONS

LG1 -(contactor 1)- LB1;
RG1 -(contactor 2)- RB1;
LB1 -(contactor 3)- RB1;

UNSWITCHED

LB1 -- LR1;
LR1 -- LD1;
LD1 -- LL1;
RB1 -- RR1;
RR1 -- RD1;
RD1 -- RL1;

REQUIREMENTS
never-connect(generator, generator, AC bus);
must-disconnect-failed(generator, 20, MS);
prefer-active-connection(left DC bus, left generator);
prefer-active-connection(right DC bus, right generator);
never-disconnect(DC bus, generator, 30, MS);
keep-connection-stable(generator, DC bus);

ASSUMPTIONS
switch-on-time(contactor 1, 10, MS);
switch-off-time(contactor 1, 10, MS);
switch-on-time(contactor 2, 10, MS);
switch-off-time(contactor 2, 10, MS);
switch-on-time(contactor 3, 10, MS);
switch-off-time(contactor 3, 10, MS);
no-recovery(generator);
max-failures(generator, 1);
no-failures(load);
no-failures(left DC bus);
no-failures(right DC bus);
no-failures(left AC bus);
no-failures(right AC bus);
no-failures(rectifier);
no-control(generator);
no-control(AC bus);
no-control(left DC bus);
no-control(right DC bus);
no-control(load);
no-control(rectifier);
initial-state(contactor 1, 1);
initial-state(contactor 2, 1);
initial-state(contactor 3, 0);
