• 设为首页
  • 点击收藏
  • 手机版
    手机扫一扫访问
    迪恩网络手机版
  • 关注官方公众号
    微信扫一扫关注
    迪恩网络公众号

Python parsing.parseATLK函数代码示例

原作者: [db:作者] 来自: [db:来源] 收藏 邀请

本文整理汇总了Python中tools.atlkFO.parsing.parseATLK函数的典型用法代码示例。如果您正苦于以下问题:Python parseATLK函数的具体用法?Python parseATLK怎么用?Python parseATLK使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。



在下文中一共展示了parseATLK函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Python代码示例。

示例1: test_counters_FSF

    def test_counters_FSF(self):
        fsm = self.counters()

        from tools.atlkPO.evalGen import split

        agents = {"a1", "a2"}
        strats = split(fsm, fsm.protocol(agents) & fsm.reachable_states, agents, semantics="individual")
        self.assertEqual(len(list(strats)), 16)

        self.assertTrue(
            check(
                fsm, parseATLK("<'a1', 'a2'> F 'v1 & v2'")[0], semantics="individual", implem="symbolic", variant="FSF"
            )
        )
        self.assertFalse(
            check(
                fsm,
                parseATLK("<'a1', 'a2'> G '!v1 & !v2'")[0],
                semantics="individual",
                implem="symbolic",
                variant="FSF",
            )
        )
        self.assertTrue(
            check(
                fsm,
                parseATLK("AG('!v1 & !v2' -> <'a1', 'a2'> G '!v1 | !v2')")[0],
                semantics="individual",
                implem="symbolic",
                variant="FSF",
            )
        )
开发者ID:sbusard,项目名称:pynusmv,代码行数:32,代码来源:testCheckIndividualSymbolic.py


示例2: test_fail

 def test_fail(self):
     kos = ["", "'test", "A<'test'>H 'q'", "O", "A<'a'>E<'e'>G 'true'",
            "E<'ac'>[A<'ac'>['a' E<'ac'>['b' W 'c'] W 'd'] "
            "U A<'ac'>['e' U 'f']]", "A<'t't'>G 'q'"]
     
     for s in kos:
         with self.assertRaises(ParseException):
             parseATLK(s)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:8,代码来源:testParsing.py


示例3: test_cardgame_post_fair_improved_symbolic

    def test_cardgame_post_fair_improved_symbolic(self):
        fsm = self.cardgame_post_fair()

        self.assertFalse(check(fsm, parseATLK("<'player'> X 'win'")[0], implem="symbolic", variant="FSF"))

        self.assertTrue(
            check(
                fsm, parseATLK("K<'player'>'pcard=none' & K<'player'>'dcard=none'")[0], implem="symbolic", variant="FSF"
            )
        )
开发者ID:sbusard,项目名称:pynusmv,代码行数:10,代码来源:testCheckSymbolic.py


示例4: test_cardgame_post_fair_not_improved

    def test_cardgame_post_fair_not_improved(self):
        fsm = self.cardgame_post_fair()

        self.assertTrue(
            check(
                fsm,
                parseATLK("K<'player'>'pcard=none' & K<'player'>'dcard=none'")[0],
                implem="symbolic",
                semantics="individual",
            )
        )
        self.assertTrue(
            check(
                fsm,
                parseATLK(
                    "AG('step = 1' -> ~(K<'player'> 'dcard=Ac' | K<'player'> 'dcard=K' | K<'player'> 'dcard=Q'))"
                )[0],
                implem="symbolic",
                semantics="individual",
            )
        )

        self.assertTrue(
            check(fsm, parseATLK("AG('step = 1' -> ~<'player'> X 'win')")[0], implem="symbolic", semantics="individual")
        )
        self.assertFalse(check(fsm, parseATLK("['dealer'] F 'win'")[0], implem="symbolic", semantics="individual"))
        self.assertTrue(check(fsm, parseATLK("['player'] X 'pcard=Ac'")[0], implem="symbolic", semantics="individual"))
        self.assertTrue(check(fsm, parseATLK("<'dealer'> X 'pcard=Ac'")[0], implem="symbolic", semantics="individual"))
        self.assertTrue(check(fsm, parseATLK("<'dealer'> G ~'win'")[0], implem="symbolic", semantics="individual"))

        # Player can win
        self.assertTrue(check(fsm, parseATLK("<'player'> F 'win'")[0], implem="symbolic", semantics="individual"))
        # Dealer can avoid fairness
        self.assertTrue(check(fsm, parseATLK("<'dealer'> F 'FALSE'")[0], implem="symbolic", semantics="individual"))
开发者ID:sbusard,项目名称:pynusmv,代码行数:34,代码来源:testCheckIndividualSymbolic.py


示例5: test_coins

 def test_coins(self):
     fsm = self.coins()
     
     from tools.atlkPO.evalGen import split
     agents = {'a1', 'a2'}
     strats = split(fsm, fsm.protocol(agents) & fsm.reachable_states,
                    agents, semantics='individual')
     self.assertEqual(len(list(strats)), 64)
     
     self.assertFalse(check(fsm, parseATLK("<'a1', 'a2'> F 'result = win'")[0], implem="generatorSI", semantics="individual"))
     self.assertFalse(check(fsm, parseATLK("<'a1', 'a2'> F 'result = win'")[0], implem="generatorSI", semantics="individual", variant="FSF"))
开发者ID:ancailliau,项目名称:pynusmv,代码行数:11,代码来源:testCheckIndividualGenSI.py


示例6: test_counters

 def test_counters(self):
     fsm = self.counters()
     
     from tools.atlkPO.evalGen import split
     agents = {'a1', 'a2'}
     strats = split(fsm, fsm.protocol(agents) & fsm.reachable_states,
                    agents, semantics='individual')
     self.assertEqual(len(list(strats)), 16)
     
     self.assertTrue(check(fsm, parseATLK("<'a1', 'a2'> F 'v1 & v2'")[0], implem="generatorSI", semantics="individual"))
     self.assertFalse(check(fsm, parseATLK("<'a1', 'a2'> G '!v1 & !v2'")[0], implem="generatorSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("AG('!v1 & !v2' -> <'a1', 'a2'> G '!v1 | !v2')")[0], implem="generatorSI", semantics="individual"))
开发者ID:ancailliau,项目名称:pynusmv,代码行数:12,代码来源:testCheckIndividualGenSI.py


示例7: test_atom

 def test_atom(self):
     s = "'c <= 3'"
     asts = parseATLK(s)
     self.assertEqual(len(asts), 1)
     
     ast = asts[0]
     self.assertTrue(isinstance(ast, Spec))
     self.assertTrue(isinstance(ast, Atom))
     self.assertEqual(ast.value, "c <= 3")
开发者ID:ancailliau,项目名称:pynusmv,代码行数:9,代码来源:testParsing.py


示例8: test_cardgame_improved

    def test_cardgame_improved(self):
        fsm = self.cardgame()

        self.assertTrue(
            check(fsm, parseATLK("<'dealer'> X 'pcard=Ac'")[0], variant="FS", implem="symbolic", semantics="individual")
        )
        self.assertFalse(
            check(fsm, parseATLK("<'dealer'> G ~'win'")[0], variant="FS", implem="symbolic", semantics="individual")
        )
        self.assertTrue(
            check(
                fsm,
                parseATLK("AG('step = 1' -> ~<'player'> X 'win')")[0],
                variant="FS",
                implem="symbolic",
                semantics="individual",
            )
        )
        self.assertFalse(
            check(fsm, parseATLK("<'player'> F 'win'")[0], variant="FS", implem="symbolic", semantics="individual")
        )

        self.assertTrue(
            check(fsm, parseATLK("['player'] X 'pcard=Ac'")[0], variant="FS", implem="symbolic", semantics="individual")
        )
        self.assertTrue(
            check(fsm, parseATLK("['dealer'] F 'win'")[0], variant="FS", implem="symbolic", semantics="individual")
        )
开发者ID:sbusard,项目名称:pynusmv,代码行数:28,代码来源:testCheckIndividualSymbolic.py


示例9: test_cardgame_post_fair_improved_symbolic2

    def test_cardgame_post_fair_improved_symbolic2(self):
        fsm = self.cardgame_post_fair()

        self.assertTrue(
            check(
                fsm,
                parseATLK(
                    "AG('step = 1' -> ~(K<'player'> 'dcard=Ac' | K<'player'> 'dcard=K' | K<'player'> 'dcard=Q'))"
                )[0],
                implem="symbolic",
                variant="FSF",
            )
        )
开发者ID:sbusard,项目名称:pynusmv,代码行数:13,代码来源:testCheckSymbolic.py


示例10: test_CEF

 def test_CEF(self):
     s = "<'agent'>F 'test'"
     asts = parseATLK(s)
     self.assertEqual(len(asts), 1)
     
     ast = asts[0]
     self.assertTrue(isinstance(ast, CEF))
     for ag in ast.group:
         self.assertTrue(isinstance(ag, Atom))
     self.assertEqual(len(ast.group), 1)
     self.assertEqual(ast.group[0].value, 'agent')
     self.assertTrue(isinstance(ast.child, Atom))
     self.assertEqual(ast.child.value, "test")
开发者ID:ancailliau,项目名称:pynusmv,代码行数:13,代码来源:testParsing.py


示例11: test_deep_spec

 def test_deep_spec(self):
     s = ("<'a','b'>[['c'][['e'] F ('p' & 'q') W K<'a'> 'p'] U <'d'>G "
          "nC<'g','e'> ('c' -> EF 'k')]")
     asts = parseATLK(s)
     self.assertEqual(len(asts), 1)
     
     ast = asts[0]
     self.assertTrue(isinstance(ast, CEU))
     
     self.assertEqual(len(ast.group), 2)
     self.assertTrue(isinstance(ast.group[0], Atom))
     self.assertEqual(ast.group[0].value, "a")
     self.assertTrue(isinstance(ast.group[1], Atom))
     self.assertEqual(ast.group[1].value, "b")
     
     self.assertTrue(isinstance(ast.left, CAW))
     self.assertEqual(len(ast.left.group), 1)
     self.assertTrue(isinstance(ast.left.group[0], Atom))
     self.assertEqual(ast.left.group[0].value, "c")
     self.assertTrue(isinstance(ast.left.left, CAF))
     self.assertEqual(len(ast.left.left.group), 1)
     self.assertTrue(isinstance(ast.left.left.group[0], Atom))
     self.assertEqual(ast.left.left.group[0].value, "e")
     self.assertTrue(isinstance(ast.left.left.child, And))
     self.assertTrue(isinstance(ast.left.left.child.left, Atom))
     self.assertEqual(ast.left.left.child.left.value, "p")
     self.assertTrue(isinstance(ast.left.left.child.right, Atom))
     self.assertEqual(ast.left.left.child.right.value, "q")
     self.assertTrue(isinstance(ast.left.right, K))
     self.assertTrue(isinstance(ast.left.right.agent, Atom))
     self.assertEqual(ast.left.right.agent.value, "a")
     self.assertTrue(isinstance(ast.left.right.child, Atom))
     self.assertEqual(ast.left.right.child.value, "p")
     
     self.assertTrue(isinstance(ast.right, CEG))
     self.assertEqual(len(ast.right.group), 1)
     self.assertTrue(isinstance(ast.right.group[0], Atom))
     self.assertEqual(ast.right.group[0].value, "d")
     self.assertTrue(isinstance(ast.right.child, nC))
     self.assertEqual(len(ast.right.child.group), 2)
     self.assertTrue(isinstance(ast.right.child.group[0], Atom))
     self.assertEqual(ast.right.child.group[0].value, "g")
     self.assertTrue(isinstance(ast.right.child.group[1], Atom))
     self.assertEqual(ast.right.child.group[1].value, "e")
     self.assertTrue(isinstance(ast.right.child.child, Implies))
     self.assertTrue(isinstance(ast.right.child.child.left, Atom))
     self.assertEqual(ast.right.child.child.left.value, "c")
     self.assertTrue(isinstance(ast.right.child.child.right, EF))
     self.assertTrue(isinstance(ast.right.child.child.right.child, Atom))
     self.assertEqual(ast.right.child.child.right.child.value, "k")
开发者ID:ancailliau,项目名称:pynusmv,代码行数:50,代码来源:testParsing.py


示例12: test_transmission_with_know_not_improved_partial

 def test_transmission_with_know_not_improved_partial(self):
     fsm = self.transmission_with_knowledge()
     
     self.assertFalse(check(fsm, parseATLK("<'sender'> F 'received'")[0], implem="partial"))
     self.assertTrue(check(fsm, parseATLK("<'transmitter'> G ~'received'")[0], implem="partial"))
     self.assertFalse(check(fsm, parseATLK("<'sender'> X 'received'")[0], implem="partial"))
     self.assertTrue(check(fsm, parseATLK("<'transmitter'> X ~'received'")[0], implem="partial"))
     self.assertFalse(check(fsm, parseATLK("<'transmitter'> F 'received'")[0], implem="partial"))
     self.assertTrue(check(fsm, parseATLK("<'sender'> G ~'received'")[0], implem="partial"))
开发者ID:ancailliau,项目名称:pynusmv,代码行数:9,代码来源:testCheckPartial.py


示例13: test_transmission_with_know_improved_symbolic

    def test_transmission_with_know_improved_symbolic(self):
        fsm = self.transmission_with_knowledge()

        self.assertTrue(check(fsm, parseATLK("<'transmitter'> G ~'received'")[0], implem="symbolic", variant="FSF"))
        self.assertFalse(check(fsm, parseATLK("<'sender'> F 'received'")[0], implem="symbolic", variant="FSF"))
        self.assertFalse(check(fsm, parseATLK("<'sender'> X 'received'")[0], implem="symbolic", variant="FSF"))
        self.assertTrue(check(fsm, parseATLK("<'transmitter'> X ~'received'")[0], implem="symbolic", variant="FSF"))
        self.assertFalse(check(fsm, parseATLK("<'transmitter'> F 'received'")[0], implem="symbolic", variant="FSF"))
        self.assertTrue(check(fsm, parseATLK("<'sender'> G ~'received'")[0], implem="symbolic", variant="FSF"))
开发者ID:sbusard,项目名称:pynusmv,代码行数:9,代码来源:testCheckSymbolic.py


示例14: test_transmission_with_know_improved

 def test_transmission_with_know_improved(self):
     fsm = self.transmission_with_knowledge()
     
     self.assertFalse(check(fsm, parseATLK("<'sender'> F 'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("<'transmitter'> G ~'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertFalse(check(fsm, parseATLK("<'sender'> X 'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("<'transmitter'> X ~'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertFalse(check(fsm, parseATLK("<'transmitter'> F 'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("<'sender'> G ~'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
开发者ID:ancailliau,项目名称:pynusmv,代码行数:9,代码来源:testCheckIndividualPartialSI.py


示例15: test_cardgame_post_fair_early_filtering

 def test_cardgame_post_fair_early_filtering(self):
     fsm = self.cardgame_post_fair()
     
     config.partial.filtering = True
     
     self.assertTrue(check(fsm, parseATLK("AG('step = 1' -> ~<'player'> X 'win')")[0], variant="FS", implem="partialSI", semantics="individual"))
     
     self.assertTrue(check(fsm, parseATLK("K<'player'>'pcard=none' & K<'player'>'dcard=none'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("AG('step = 1' -> ~(K<'player'> 'dcard=Ac' | K<'player'> 'dcard=K' | K<'player'> 'dcard=Q'))")[0], variant="FS", implem="partialSI", semantics="individual"))
     
     self.assertFalse(check(fsm, parseATLK("['dealer'] F 'win'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("['player'] X 'pcard=Ac'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("<'dealer'> X 'pcard=Ac'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("<'dealer'> G ~'win'")[0], variant="FS", implem="partialSI", semantics="individual"))
     
     # Player can win
     self.assertTrue(check(fsm, parseATLK("<'player'> F 'win'")[0], variant="FS", implem="partialSI", semantics="individual"))
     # Dealer can avoid fairness
     self.assertTrue(check(fsm, parseATLK("<'dealer'> F 'FALSE'")[0], variant="FS", implem="partialSI", semantics="individual"))
     
     config.partial.filtering = False
开发者ID:ancailliau,项目名称:pynusmv,代码行数:21,代码来源:testCheckIndividualPartialSIFSFiltering.py


示例16: test_transmission_with_know_improved_partial_strat_only

 def test_transmission_with_know_improved_partial_strat_only(self):
     fsm = self.transmission_with_knowledge()
     config.partial.alternate.type = {"strat"}
     
     self.assertTrue(check(fsm, parseATLK("<'transmitter'> G ~'received'")[0], implem="partial", variant="FS"))
     self.assertFalse(check(fsm, parseATLK("<'sender'> F 'received'")[0], implem="partial", variant="FS"))
     self.assertFalse(check(fsm, parseATLK("<'sender'> X 'received'")[0], implem="partial", variant="FS"))
     self.assertTrue(check(fsm, parseATLK("<'transmitter'> X ~'received'")[0], implem="partial", variant="FS"))
     self.assertFalse(check(fsm, parseATLK("<'transmitter'> F 'received'")[0], implem="partial", variant="FS"))
     self.assertTrue(check(fsm, parseATLK("<'sender'> G ~'received'")[0], implem="partial", variant="FS"))
开发者ID:ancailliau,项目名称:pynusmv,代码行数:10,代码来源:testCheckPartial.py


示例17: test_transmission_post_fair_improved

 def test_transmission_post_fair_improved(self):
     fsm = self.transmission_post_fair()
     
     self.assertTrue(check(fsm, parseATLK("<'sender'> F 'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("<'transmitter'> G ~'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertFalse(check(fsm, parseATLK("<'sender'> X 'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("<'transmitter'> X ~'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("<'transmitter'> F 'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
     
     # False because the sender does not know if the bit is already
     # transmitted (and in this case, no strategy can avoid 'received')
     self.assertFalse(check(fsm, parseATLK("<'sender'> G ~'received'")[0], variant="FS", implem="partialSI", semantics="individual"))
开发者ID:ancailliau,项目名称:pynusmv,代码行数:12,代码来源:testCheckIndividualPartialSI.py


示例18: test_cardgame_early_filtering

 def test_cardgame_early_filtering(self):
     fsm = self.cardgame()
     
     config.partial.filtering = True
     self.assertFalse(check(fsm, parseATLK("<'player'> F 'win'")[0], variant="FS", implem="partialSI", semantics="individual"))        
     self.assertTrue(check(fsm, parseATLK("AG('step = 1' -> ~<'player'> X 'win')")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("<'dealer'> X 'pcard=Ac'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertFalse(check(fsm, parseATLK("<'dealer'> G ~'win'")[0], variant="FS", implem="partialSI", semantics="individual"))
     
     self.assertTrue(check(fsm, parseATLK("['player'] X 'pcard=Ac'")[0], variant="FS", implem="partialSI", semantics="individual"))
     self.assertTrue(check(fsm, parseATLK("['dealer'] F 'win'")[0], variant="FS", implem="partialSI", semantics="individual"))
     
     config.partial.filtering = False
开发者ID:ancailliau,项目名称:pynusmv,代码行数:13,代码来源:testCheckIndividualPartialSIFSFiltering.py


示例19: test_transmission_improved

    def test_transmission_improved(self):
        fsm = self.transmission()

        # False because transmitter cannot win if received is already true
        # and he has no clue about it
        self.assertFalse(
            check(
                fsm,
                parseATLK("<'transmitter'> G ~'received'")[0],
                variant="FS",
                implem="symbolic",
                semantics="individual",
            )
        )
        self.assertFalse(
            check(fsm, parseATLK("<'sender'> X 'received'")[0], variant="FS", implem="symbolic", semantics="individual")
        )
        # False because transmitter cannot win if received is already true
        # and he has no clue about it
        self.assertFalse(
            check(
                fsm,
                parseATLK("<'transmitter'> X ~'received'")[0],
                variant="FS",
                implem="symbolic",
                semantics="individual",
            )
        )

        # False because the sender does not know if the bit is already
        # transmitted (and in this case, no strategy can avoid 'received')
        self.assertFalse(
            check(
                fsm, parseATLK("<'sender'> G ~'received'")[0], variant="FS", implem="symbolic", semantics="individual"
            )
        )

        self.assertFalse(
            check(
                fsm,
                parseATLK("<'transmitter'> F 'received'")[0],
                variant="FS",
                implem="symbolic",
                semantics="individual",
            )
        )
        self.assertFalse(
            check(fsm, parseATLK("<'sender'> F 'received'")[0], variant="FS", implem="symbolic", semantics="individual")
        )
开发者ID:sbusard,项目名称:pynusmv,代码行数:49,代码来源:testCheckIndividualSymbolic.py


示例20: test_tpfni_partial_vs_normal

 def test_tpfni_partial_vs_normal(self):
     fsm = self.transmission_post_fair()
     
     self.assertTrue(check(fsm, parseATLK("<'sender'> F 'received'")[0]))
     self.assertTrue(check(fsm, parseATLK("<'sender'> F 'received'")[0], implem="partial"))
开发者ID:ancailliau,项目名称:pynusmv,代码行数:5,代码来源:testCheckPartial.py



注:本文中的tools.atlkFO.parsing.parseATLK函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。


鲜花

握手

雷人

路过

鸡蛋
该文章已有0人参与评论

请发表评论

全部评论

专题导读
上一篇:
Python check.check函数代码示例发布时间:2022-05-27
下一篇:
Python assertions.assert_one函数代码示例发布时间:2022-05-27
热门推荐
阅读排行榜

扫描微信二维码

查看手机版网站

随时了解更新最新资讯

139-2527-9053

在线客服(服务时间 9:00~18:00)

在线QQ客服
地址:深圳市南山区西丽大学城创智工业园
电邮:jeky_zhao#qq.com
移动电话:139-2527-9053

Powered by 互联科技 X3.4© 2001-2213 极客世界.|Sitemap