test_temporallogic.py 文件源码

def test_negationnormalform(self):
        self.assertEqual(NOT(AP("a")).negationnormalform(), NOT(AP("a")))
        self.assertEqual(NOT(NOT(AP("a"))).negationnormalform(), AP("a"))
        self.assertEqual(NOT(NEXT(AP("a"))).negationnormalform(), NEXT(NOT(AP("a"))))
        self.assertEqual(NOT(AP(None, None, operator.ge, 42, 'x')).negationnormalform(),
                         AP(None, None, operator.lt, 42, 'x'))
        self.assertEqual(NOT(AP(None, None, operator.le, 42, 'x')).negationnormalform(),
                         AP(None, None, operator.gt, 42, 'x'))
        self.assertEqual(NOT(AP(None, None, operator.gt, 42, 'x')).negationnormalform(),
                         AP(None, None, operator.le, 42, 'x'))
        self.assertEqual(NOT(AP(None, None, operator.lt, 42, 'x')).negationnormalform(),
                         AP(None, None, operator.ge, 42, 'x'))
        self.assertEqual(NOT(AP(None, None, operator.eq, 42, 'x')).negationnormalform(),
                         AP(None, None, operator.ne, 42, 'x'))
        self.assertEqual(NOT(AP(None, None, operator.ne, 42, 'x')).negationnormalform(),
                         AP(None, None, operator.eq, 42, 'x'))
        self.assertEqual(NOT(AND(AP("a"), AP("b"))).negationnormalform(), OR(NOT(AP("a")), NOT(AP("b"))))
        self.assertEqual(NOT(OR(AP("a"), AP("b"))).negationnormalform(), AND(NOT(AP("a")), NOT(AP("b"))))
        self.assertEqual(NOT(IMPLIES(AP("a"), AP("b"))).negationnormalform(), AND(AP("a"), NOT(AP("b"))))