Files required for the verification of an ethical robots using the AJPF model checker as discussed in the paper Bremner et al `On Proactive, Transparent and VerifiableEthical Reasoning for Robots' to appear in IEEE transactions.