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)

 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)))

    def counters(self):
        # Build model
        class main(Module):
            v1 = Var(Boolean())
            v2 = Var(Boolean())

            act1 = IVar(Scalar(("skip", "inc")))
            act2 = IVar(Scalar(("skip", "inc")))

            TRANS = [v1.next() == (act1 == "skip").ite(v1, ~v1)]
            TRANS += [v2.next() == (act2 == "skip").ite(v2, ~v2)]

        # Define agents
        a1 = Agent("a1", {main.v1}, {main.act1})
        a2 = Agent("a2", {main.v2}, {main.act2})
        g = Group("g", a1, a2)

        # Load model
        glob.load(main)

        # Get MAS
        mas = glob.mas({a1, a2, g})
        
        self.assertIsNotNone(mas)
        return mas

 def test_dining_crypto(self):
     glob.load_from_file("tests/tools/ctlk/dining-crypto.smv")
     fsm = glob.mas()
     self.assertIsNotNone(fsm)
     
     agents = fsm._epistemic.keys()
     self.assertSetEqual(set(agents), {"c1", "c2", "c3"})

 def test_cardgame_with_agents(self):
     glob.load_from_file("tests/tools/mas/cardgame.smv")
     agents = (Agent("player", {"step", "pcard", "ddcard"},
                     {"player.action"}),
               Agent("dealer", {"step", "pcard", "dcard"},
                     {"dealer.action"}))
     fsm = glob.mas(agents=agents)
     self.assertIsNotNone(fsm)
     return fsm

    def coins(self):
        # Build model
        class main(Module):
            c1 = Var(Scalar(("none", "head", "tail")))
            c2 = Var(Scalar(("none", "head", "tail")))
            result = Var(Scalar(("none", "win", "lose")))

            act1 = IVar(Scalar(("different", "equal")))
            act2 = IVar(Scalar(("different", "equal")))

            INIT = [(c1 == "none") & (c2 == "none") & (result == "none")]

            TRANS = []

            TRANS += [
                ((c1 == "none") & (c2 == "none")).implies(
                    c1.next().in_(Set(("head", "tail")))
                    & c2.next().in_(Set(("head", "tail")))
                    & (result.next() == result)
                )
            ]
            TRANS += [
                ((c1 != "none") & (c2 != "none") & (result == "none")).implies(
                    (c1.next() == c1)
                    & (c2.next() == c2)
                    & (
                        result.next()
                        == (
                            ((c1 == c2) & (act1 == "equal") & (act2 == "equal"))
                            | ((c1 != c2) & (act1 == "different") & (act2 == "different"))
                        ).ite("win", "lose")
                    )
                )
            ]
            TRANS += [(result != "none").implies((result.next() == result) & (c1.next() == c1) & (c2.next() == c2))]

        # Define agents
        a1 = Agent("a1", {main.c1}, {main.act1})
        a2 = Agent("a2", {main.c2}, {main.act2})
        g = Group("g", a1, a2)

        # Load model
        glob.load(main)

        # Get MAS
        mas = glob.mas({a1, a2, g})

        self.assertIsNotNone(mas)
        return mas

 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))

 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)

 def test_check_mas_uniform_choice_ok(self):
     class agent(md.Module):
         v = md.Var(md.Boolean())
         a = md.IVar(md.Boolean())
         INIT = v
         TRANS = (v.next() == a)
     class main(md.Module):
         a1 = md.Var(agent())
         a2 = md.Var(agent())
     
     agents = {Agent("a1", {main.a1.v}, {main.a1.a}),
               Agent("a2", {main.a2.v}, {main.a2.a})}
     
     glob.load(agent, main)
     mas = glob.mas(agents=agents)
     self.assertIsNotNone(mas)
     self.assertTrue(mas.check_uniform_choice().is_false())

 def test_next_state_without_inputs(self):
     glob.load_from_file("tests/pynusmv/models/modules.smv")
     fsm = glob.mas()
     self.assertIsNotNone(fsm)
     c2p = eval_simple_expression(fsm, "top")
     (inputs, state) = choose_next_state(fsm, fsm.pick_one_state(fsm.init))
     
     print()
     if state is None:
         print("No chosen state.")
     else:
         if inputs is not None:
             values = inputs.get_str_values()
             for var in values:
                 print(var, "=", values[var])
             print("-" * 40)
         values = state.get_str_values()
         for var in values:
             print(var, "=", values[var])

 def test_check_mas_free_choice_ko(self):
     class agent(md.Module):
         v = md.Var(md.Boolean())
         a = md.IVar(md.Boolean())
         INIT = v
         TRANS = (v.next() == a)
     class main(md.Module):
         a1 = md.Var(agent())
         a2 = md.Var(agent())
         TRANS = a2.a.implies(a1.a)
     
     agents = {Agent("a1", {main.a1.v, main.a2.v}, {main.a1.a}),
               Agent("a2", {main.a1.v, main.a2.v}, {main.a2.a})}
     
     glob.load(agent, main)
     mas = glob.mas(agents=agents)
     self.assertIsNotNone(mas)
     
     free_choice = mas.check_free_choice()
     self.assertTrue(free_choice.isnot_false())

 def do_model(self, arg):
     if "model" not in self.argparsers:
         self.parse_model()
     
     # Handle arguments parsing errors
     try:
         args = self.argparsers["model"].parse_args(self._split_escaped(arg))
     except ArgumentParsingError as err:
         print(err, end="")
         return False
     
     # Error if
     #   showing path or content when nothing is read
     #   reading a file when one is already read
     
     if (args.content or args.path is None) and self.model is None:
         print("No read model.")
         return False
     
     if args.path is not None and self.model is not None:
         print("model: error: a model is already read from", self.model.path)
         return False
         
     if args.path is None:
         print("read model:", self.model.path)
         
     if args.content:
         print(self.model.content)
         
     if args.path is not None:
         try:
             f = open(args.path, 'r')
             content = f.read()
             f.close()
             glob.load_from_file(args.path)
             self.fsm = glob.mas()
             self.model = Model(args.path, content)
         except PyNuSMVError as err:
             print("model: error:", err)
         except IOError as err:
             print("model: error:", err)

 def model(self):
     glob.load_from_file("tests/tools/ctlk/dining-crypto.smv")
     fsm = glob.mas()
     self.assertIsNotNone(fsm)
     return fsm

 def simplemodel(self):
     glob.load_from_file("tests/tools/ctlk/agents.smv")
     fsm = glob.mas()
     self.assertIsNotNone(fsm)
     return fsm

 def transmission_fair(self):
     glob.load_from_file("tests/tools/atlkFO/models/transmission-fair.smv")
     fsm = glob.mas()
     self.assertIsNotNone(fsm)
     return fsm

 def cardgame_fair(self):
     glob.load_from_file("tests/tools/atlkFO/models/cardgame-fair.smv")
     fsm = glob.mas()
     self.assertIsNotNone(fsm)
     return fsm

 def little(self):
     glob.load_from_file("tests/tools/atlkPO/models/little.smv")
     fsm = glob.mas()
     self.assertIsNotNone(fsm)
     return fsm

 def transmission_with_knowledge(self):
     glob.load_from_file(
                     "tests/tools/atlkPO/models/transmission-knowledge.smv")
     fsm = glob.mas()
     self.assertIsNotNone(fsm)
     return fsm

 def cardgame(self):
     glob.load_from_file("tests/tools/mas/cardgame.smv")
     fsm = glob.mas()
     self.assertIsNotNone(fsm)
     return fsm

 def nfair_model(self):
     glob.load_from_file("tests/tools/atlkPO/models/nfair.smv")
     fsm = glob.mas()
     self.assertIsNotNone(fsm)
     return fsm