本文整理汇总了Python中pynusmv.mc.eval_simple_expression函数的典型用法代码示例。如果您正苦于以下问题:Python eval_simple_expression函数的具体用法?Python eval_simple_expression怎么用?Python eval_simple_expression使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了eval_simple_expression函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Python代码示例。
示例1: test_eu_simple
def test_eu_simple(self):
fsm = self.simplemodel()
lt = eval_simple_expression(fsm, "at.local")
lf = eval_simple_expression(fsm, "af.local")
g = eval_simple_expression(fsm, "global")
true = eval_simple_expression(fsm, "TRUE")
false = eval_simple_expression(fsm, "FALSE")
# lt & lf & g |= E[ g U ~lf & ~lt & ~g ]
eus = eu(fsm, g, ~lf & ~lt & ~g)
state = fsm.pick_one_state(eus)
witness = explain_eu(fsm, state, g, ~lf & ~lt & ~g)
self.assertTrue(witness[0] == state)
self.assertTrue(witness[0] <= g | ~lf & ~lt & ~g)
for (s, i, sp) in zip(witness[:-2:2], witness[1:-2:2], witness[2:-2:2]):
self.assertTrue(s <= g)
self.assertTrue(sp <= g)
self.assertIsNotNone(i)
self.assertTrue(i <= fsm.get_inputs_between_states(s, sp))
self.assertIsNotNone(witness[-2])
self.assertTrue(witness[-2] <=
fsm.get_inputs_between_states(witness[-3], witness[-1]))
self.assertTrue(witness[-1] <= ~lf)
self.assertTrue(witness[-1] <= ~lt)
self.assertTrue(witness[-1] <= ~g)
self.assertTrue(witness[-1] == ~lf & ~lt & ~g)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:29,代码来源:testExplain.py
示例2: test_eg_simple
def test_eg_simple(self):
fsm = self.simplemodel()
lt = eval_simple_expression(fsm, "at.local")
lf = eval_simple_expression(fsm, "af.local")
g = eval_simple_expression(fsm, "global")
true = eval_simple_expression(fsm, "TRUE")
false = eval_simple_expression(fsm, "FALSE")
# lt & lf & !g |= EG !g
egs = eg(fsm, ~g)
self.assertTrue(egs.isnot_false())
state = fsm.pick_one_state(egs)
(path, loop) = explain_eg(fsm, state, ~g)
self.assertTrue(path[0] == state)
self.assertTrue(path[0] <= ~g & egs)
for (s, i, sp) in zip(path[::2], path[1::2], path[2::2]):
self.assertTrue(s <= ~g)
self.assertTrue(sp <= ~g)
self.assertIsNotNone(i)
self.assertTrue(i <= fsm.get_inputs_between_states(s, sp))
self.assertIsNotNone(loop)
self.assertEqual(len(loop), 2)
self.assertIsNotNone(loop[0])
self.assertIsNotNone(loop[1])
self.assertTrue(loop[1] in path)
self.assertTrue(loop[0] <=
fsm.get_inputs_between_states(path[-1], loop[1]))
开发者ID:ancailliau,项目名称:pynusmv,代码行数:31,代码来源:testExplain.py
示例3: test_constraints_post
def test_constraints_post(self):
glob.load_from_file("tests/tools/ctlk/constraints.smv")
fsm = glob.mas()
self.assertIsNotNone(fsm)
false = eval_simple_expression(fsm, "FALSE")
false = eval_simple_expression(fsm, "TRUE")
p = eval_simple_expression(fsm, "p")
q = eval_simple_expression(fsm, "q")
a = eval_simple_expression(fsm, "a")
self.assertEqual(1, fsm.count_states(fsm.init))
self.assertEqual(2, fsm.count_states(fsm.post(fsm.init)))
self.assertEqual(1, fsm.count_states(p & q))
self.assertEqual(1, fsm.count_states(p & ~q))
self.assertEqual(1, fsm.count_states(~p & q))
self.assertEqual(1, fsm.count_states(~p & ~q))
self.assertEqual(2, fsm.count_states(fsm.post(p & q)))
self.assertEqual(1, fsm.count_states(fsm.post(p & ~q)))
self.assertEqual(1, fsm.count_states(fsm.post(~p & q)))
self.assertEqual(1, fsm.count_states(fsm.post(p & q, a)))
self.assertEqual(0, fsm.count_states(fsm.post(p & ~q, ~a)))
self.assertEqual(0, fsm.count_states(fsm.post(~p & q, a)))
self.assertEqual(1, fsm.count_states(fsm.post(~p & q, ~a)))
开发者ID:ancailliau,项目名称:pynusmv,代码行数:25,代码来源:testMAS.py
示例4: test_k
def test_k(self):
fsm = self.simplemodel()
lt = eval_simple_expression(fsm, "at.local")
lf = eval_simple_expression(fsm, "af.local")
g = eval_simple_expression(fsm, "global")
true = eval_simple_expression(fsm, "TRUE")
false = eval_simple_expression(fsm, "FALSE")
specs = parseCTLK("K<'at'> 'at.local'")
self.assertEqual(len(specs), 1)
spec = specs[0]
katt = evalCTLK(fsm, spec)
self.assertEqual(katt, lt)
specs = parseCTLK("K<'at'> 'af.local'")
self.assertEqual(len(specs), 1)
spec = specs[0]
katf = evalCTLK(fsm, spec)
self.assertEqual(katf, false)
specs = parseCTLK("K<'at'> 'global'")
self.assertEqual(len(specs), 1)
spec = specs[0]
katf = evalCTLK(fsm, spec)
self.assertEqual(katf, g)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:26,代码来源:testEval.py
示例5: test_d_simple
def test_d_simple(self):
fsm = self.simplemodel()
lt = eval_simple_expression(fsm, "at.local")
lf = eval_simple_expression(fsm, "af.local")
g = eval_simple_expression(fsm, "global")
true = eval_simple_expression(fsm, "TRUE")
false = eval_simple_expression(fsm, "FALSE")
specs = parseCTLK("'af.local' -> D<'at','af'> 'af.local'")
self.assertEqual(len(specs), 1)
spec = specs[0]
geg = evalCTLK(fsm, spec)
self.assertEqual(geg, true)
specs = parseCTLK("'af.local' & D<'at'> 'af.local'")
self.assertEqual(len(specs), 1)
spec = specs[0]
geg = evalCTLK(fsm, spec)
self.assertEqual(geg, false)
specs = parseCTLK("'af.local' -> D<'af'> 'af.local'")
self.assertEqual(len(specs), 1)
spec = specs[0]
geg = evalCTLK(fsm, spec)
self.assertEqual(geg, true)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:26,代码来源:testEval.py
示例6: test_nfair_si_nfair_model
def test_nfair_si_nfair_model(self):
fsm = self.nfair_model()
s0 = eval_simple_expression(fsm, "state = s0")
s1 = eval_simple_expression(fsm, "state = s1")
s2 = eval_simple_expression(fsm, "state = s2")
a0 = eval_simple_expression(fsm, "a.a = 0")
a1 = eval_simple_expression(fsm, "a.a = 1")
a2 = eval_simple_expression(fsm, "a.a = 2")
b0 = eval_simple_expression(fsm, "b.a = 0")
b1 = eval_simple_expression(fsm, "b.a = 1")
true = eval_simple_expression(fsm, "TRUE")
false = eval_simple_expression(fsm, "FALSE")
nfgsia = nfair_gamma_si(fsm, {"a"})
nfgsib = nfair_gamma_si(fsm, {"b"})
self.assertTrue(s0 & a1 & fsm.protocol({"a"}) <= nfgsia)
self.assertTrue(s1 & a0 & fsm.protocol({"a"}) <= nfgsia)
self.assertEqual((s0 & a1 & fsm.protocol({"a"})) | (s1 & a0 & fsm.protocol({"a"})), nfgsia)
self.assertEqual(s1 & b0 & fsm.protocol({"b"}), nfgsib)
开发者ID:sbusard,项目名称:pynusmv,代码行数:25,代码来源:testEval.py
示例7: test_minimize
def test_minimize(self):
(fsm, enc, manager) = self.init_model()
noadmin = eval_simple_expression(fsm, "admin = none")
processing = eval_simple_expression(fsm, "state = processing")
self.assertIsNotNone(processing.minimize(noadmin))
self.assertTrue(processing.minimize(noadmin).isnot_false())
开发者ID:xgillard,项目名称:pynusmv,代码行数:8,代码来源:testBDD.py
示例8: test_equivalent_states
def test_equivalent_states(self):
fsm = self.model()
c1p = eval_simple_expression(fsm, "c1.payer")
odd = eval_simple_expression(fsm, "countsay = odd")
true = eval_simple_expression(fsm, "TRUE")
self.assertEqual(fsm.equivalent_states(c1p, {"c1"}), c1p)
self.assertEqual(fsm.equivalent_states(c1p, {"c2"}), true)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:9,代码来源:testMAS.py
示例9: test_iff
def test_iff(self):
fsm = self.model()
c1p = eval_simple_expression(fsm, "c1.payer")
odd = eval_simple_expression(fsm, "countsay = odd")
specs = parseCTLK("'c1.payer' <-> 'countsay = odd'")
self.assertEqual(len(specs), 1)
spec = specs[0]
c1pico = evalCTLK(fsm, spec)
self.assertEqual(c1p.iff(odd), c1pico)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:12,代码来源:testEval.py
示例10: test_pre
def test_pre(self):
fsm = self.model()
c1p = eval_simple_expression(fsm, "c1.payer")
unknown = eval_simple_expression(fsm, "countsay = unknown")
odd = eval_simple_expression(fsm, "countsay = odd")
even = eval_simple_expression(fsm, "countsay = even")
true = eval_simple_expression(fsm, "TRUE")
self.assertTrue(odd & fsm.bddEnc.statesMask <= fsm.pre(odd))
self.assertTrue(fsm.init <= unknown)
self.assertTrue(fsm.pre(unknown).is_false())
开发者ID:ancailliau,项目名称:pynusmv,代码行数:12,代码来源:testMAS.py
示例11: test_k_ef
def test_k_ef(self):
fsm = self.simplemodel()
lt = eval_simple_expression(fsm, "at.local")
lf = eval_simple_expression(fsm, "af.local")
g = eval_simple_expression(fsm, "global")
true = eval_simple_expression(fsm, "TRUE")
specs = parseCTLK("K<'at'> EF 'af.local'")
self.assertEqual(len(specs), 1)
spec = specs[0]
kef = evalCTLK(fsm, spec)
self.assertEqual(kef, true)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:13,代码来源:testEval.py
示例12: test_ex
def test_ex(self):
fsm = self.model()
c1p = eval_simple_expression(fsm, "c1.payer")
c2p = eval_simple_expression(fsm, "c2.payer")
c3p = eval_simple_expression(fsm, "c3.payer")
c1h = eval_simple_expression(fsm, "c1.coin = head")
c2h = eval_simple_expression(fsm, "c2.coin = head")
c3h = eval_simple_expression(fsm, "c3.coin = head")
odd = eval_simple_expression(fsm, "countsay = odd")
unk = eval_simple_expression(fsm, "countsay = unknown")
specs = parseCTLK("EX ('c1.payer' & ~'c2.payer' & ~'c3.payer')")
self.assertEqual(len(specs), 1)
spec = specs[0]
ex = evalCTLK(fsm, spec)
self.assertEqual(ex, c1p & ~c2p & ~c3p & fsm.bddEnc.statesMask)
specs = parseCTLK("EX 'countsay = odd'")
self.assertEqual(len(specs), 1)
spec = specs[0]
ex = evalCTLK(fsm, spec)
self.assertTrue(odd & fsm.bddEnc.statesMask <= ex)
self.assertTrue((unk & c1p & ~c2p & ~c3p) & fsm.bddEnc.statesMask
<= ex)
self.assertTrue((unk & c1p & c2p & c3p) & fsm.bddEnc.statesMask
<= ex)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:28,代码来源:testEval.py
示例13: test_simple_pre
def test_simple_pre(self):
glob.load_from_file("tests/tools/ctlk/agents.smv")
fsm = glob.mas()
self.assertIsNotNone(fsm)
lt = eval_simple_expression(fsm, "at.local")
lf = eval_simple_expression(fsm, "af.local")
g = eval_simple_expression(fsm, "global")
true = eval_simple_expression(fsm, "TRUE")
false = eval_simple_expression(fsm, "FALSE")
self.assertEqual(fsm.pre(lt & ~lf & ~g),
(lt & lf & ~g) | (~lt & ~lf & g))
self.assertEqual(fsm.pre(g), true)
self.assertEqual(fsm.pre(lf), lf.iff(g))
开发者ID:ancailliau,项目名称:pynusmv,代码行数:15,代码来源:testMAS.py
示例14: test_reachable_states_for_simple_model
def test_reachable_states_for_simple_model(self):
glob.load_from_file("tests/tools/ctlk/agents.smv")
fsm = glob.mas()
self.assertIsNotNone(fsm)
true = eval_simple_expression(fsm, "TRUE")
self.assertEqual(fsm.reachable_states, true)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:7,代码来源:testMAS.py
示例15: test_d_distributedmodel
def test_d_distributedmodel(self):
glob.load_from_file("tests/tools/ctlk/distributed_knowledge.smv")
fsm = glob.mas()
self.assertIsNotNone(fsm)
l1 = eval_simple_expression(fsm, "a1.local")
l2 = eval_simple_expression(fsm, "a2.local")
l3 = eval_simple_expression(fsm, "a3.local")
true = eval_simple_expression(fsm, "TRUE")
false = eval_simple_expression(fsm, "FALSE")
specs = parseCTLK("'a1.local' -> D<'a1','a2'> 'a1.local'")
self.assertEqual(len(specs), 1)
spec = specs[0]
a1da1 = evalCTLK(fsm, spec)
self.assertEqual(true, a1da1)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:16,代码来源:testEval.py
示例16: test_simple
def test_simple(self):
mas = self.simple()
s4 = eval_simple_expression(mas, "s = 4")
ac = mas.bddEnc.cube_for_inputs_vars("a")
bc = mas.bddEnc.cube_for_inputs_vars("b")
self.assertTrue((~(mas.weak_pre(~s4).forsome(bc)) &
mas.weak_pre(s4)).forsome(mas.bddEnc.inputsCube))
开发者ID:ancailliau,项目名称:pynusmv,代码行数:7,代码来源:testMAS.py
示例17: test_hashes
def test_hashes(self):
(fsm, enc, manager) = self.init_model()
true = BDD.true(manager)
false = BDD.false(manager)
init = fsm.init
noadmin = eval_simple_expression(fsm, "admin = none")
alice = eval_simple_expression(fsm, "admin = alice")
processing = eval_simple_expression(fsm, "state = processing")
self.assertEqual(hash(true), hash(~false))
self.assertNotEqual(hash(true), hash(false))
self.assertEqual(hash(init & noadmin), hash(init))
bdddict = {true, false, init, noadmin, alice, processing}
self.assertEqual(len(bdddict), 6)
开发者ID:xgillard,项目名称:pynusmv,代码行数:16,代码来源:testBDD.py
示例18: test_size
def test_size(self):
(fsm, enc, manager) = self.init_model()
true = BDD.true(manager)
false = BDD.false(manager)
init = fsm.init
noadmin = eval_simple_expression(fsm, "admin = none")
alice = eval_simple_expression(fsm, "admin = alice")
processing = eval_simple_expression(fsm, "state = processing")
self.assertEqual(BDD.true().size, 1)
self.assertEqual(BDD.false().size, 1)
self.assertEqual(fsm.pick_one_state(BDD.true()).size,
len(fsm.bddEnc.get_variables_ordering("bits")) + 1)
self.assertEqual(init.size, 5)
self.assertEqual(processing.size, 3)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:15,代码来源:testBDD.py
示例19: test_uncomparable_sets
def test_uncomparable_sets(self):
(fsm, enc, manager) = self.init_model()
alice = eval_simple_expression(fsm, "admin = alice")
processing = eval_simple_expression(fsm, "state = processing")
self.assertFalse(alice <= processing)
self.assertFalse(processing <= alice)
self.assertFalse(alice < processing)
self.assertFalse(processing < alice)
self.assertFalse(alice == processing)
self.assertTrue(alice != processing)
self.assertFalse(alice >= processing)
self.assertFalse(processing >= alice)
self.assertFalse(alice > processing)
self.assertFalse(processing > alice)
开发者ID:xgillard,项目名称:pynusmv,代码行数:16,代码来源:testBDD.py
示例20: test_cardgame_cax
def test_cardgame_cax(self):
fsm = self.cardgame()
spec = parseATL("['player']X 'pcard = Ac'")[0]
agents = {atom.value for atom in spec.group}
phi = evalATL(fsm, spec.child)
self.assertTrue(check(fsm, spec))
sat = evalATL(fsm, spec)
initsat = sat & fsm.init
first = fsm.pick_one_state(initsat)
explanation = explain_cax(fsm, first, agents, evalATL(fsm, spec.child))
#self.show_cex(explanation, spec)
self.check_cax(fsm, explanation, agents, phi)
spec = parseATL("['dealer']X 'win'")[0]
agents = {atom.value for atom in spec.group}
phi = evalATL(fsm, spec.child)
# False since we do not want initial states
#self.assertTrue(check(fsm, spec))
sat = evalATL(fsm, spec)
initsat = (sat & eval_simple_expression(fsm, 'step = 1') &
fsm.reachable_states)
first = fsm.pick_one_state(initsat)
explanation = explain_cax(fsm, first, agents, evalATL(fsm, spec.child))
#self.show_cex(explanation, spec)
self.check_cax(fsm, explanation, agents, phi)
开发者ID:ancailliau,项目名称:pynusmv,代码行数:26,代码来源:testExplain.py
注:本文中的pynusmv.mc.eval_simple_expression函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论