cat_sitting.conf

settings basic_blocks_filename=basic_blocks.smv output_filename=out.smv
add_requirements filename=requirements.smv

# single unit group
unit_group name=CAT_SITTING divisions=3 failing_division=2

input in=CAT_SITTING name=WIDTH  nusmv_type=0..1000
input in=CAT_SITTING name=HEIGHT nusmv_type=0..1000
input in=CAT_SITTING name=DEPTH  nusmv_type=0..1000

output in=CAT_SITTING name=CAN_SIT

unit in=CAT_SITTING name=APU filename=apu.smv nusmv_module_name=SITTING_APU max_delay=${DELAY_APU} nusmv_outputs=CAN_SIT:boolean single_division_to_retain=NA
unit in=CAT_SITTING name=ALU filename=alu.smv nusmv_module_name=SITTING_ALU max_delay=${DELAY_ALU} nusmv_outputs=CAN_SIT:boolean single_division_to_retain=1

# determinism check (dummy symmetry)
symmetry group=CAT_SITTING unit=APU input_variable_indices=1

# the ALU is symmetric w.r.t. votes from APUs
symmetry group=CAT_SITTING unit=ALU input_variable_indices=1,2,3

# connections to APUs
parallel_connection from=input.WIDTH  to=CAT_SITTING.APU
parallel_connection from=input.HEIGHT to=CAT_SITTING.APU
parallel_connection from=input.DEPTH  to=CAT_SITTING.APU

# connections to ALUs
all_to_all_connection from=CAT_SITTING.APU.CAN_SIT to=CAT_SITTING.ALU

# connections to outputs
parallel_connection from=CAT_SITTING.ALU.CAN_SIT to=output.CAN_SIT