mod SIMPLE-SYS is sort System . ops s0 s1 s2 s3 s4 s5 s6 : -> System [ctor] . rl s0 => s1 . rl s1 => s2 . rl s2 => s3 . rl s3 => s4 . rl s4 => s3 . rl s0 => s5 . rl s5 => s6 . endm load model-checker.maude mod SIMPLE-SYS-PREDS is protecting SIMPLE-SYS . including SATISFACTION . subsort System < State . ops a b c : -> Prop . eq s0 |= a = false . eq s0 |= b = false . eq s0 |= c = false . eq s1 |= a = false . eq s1 |= b = true . eq s1 |= c = false . eq s2 |= a = true . eq s2 |= b = false . eq s2 |= c = false . eq s3 |= a = false . eq s3 |= b = true . eq s3 |= c = false . eq s4 |= a = false . eq s4 |= b = false . eq s4 |= c = true . eq s5 |= a = false . eq s5 |= b = false . eq s5 |= c = true . eq s6 |= a = true . eq s6 |= b = false . eq s6 |= c = false . endm mod SIMPLE-SYS-CHECK is protecting SIMPLE-SYS-PREDS . including MODEL-CHECKER . endm *** give here your eight model checking commands in the order listed above