Menu
Home
What's this about?
Contact
SENSEI – the Specification ENgineering Sparring partnEr (Interactive)
Specification
[Test] Spec: (a | G a) U b Neg: (a,b)=((1,0))^omega Pos: (a,b)=(0,1)((0,0))^omega Pos: (a,b)=(1,0)(0,1)((0,0))^omega [Assumption] Spec: (a U b) | G a Pos: (a,b)=(1,1)(0,0)((0,0))^omega Neg: (a,b)=(0,0)(0,0)((1,0))^omega Pos: (a,b)=(1,1)(0,0)((1,0))^omega Pos: (a,b)=((1,0))^omega [Guarantee] Spec: (a U c) | c Pos: (a,c)=(1,1)(0,0)((0,0))^omega Neg: (a,c)=(0,0)(0,0)((1,0))^omega Pos: (a,c)=(1,1)(0,0)((1,0))^omega