Feat: distributed knowledge

[foxyseta]

Closes #24:

• language 276f5b6
• lexer, parser d071383
• Explicit.K 991091e
• Explicit.S5 991091e
• Symbolic.K 9324f78
• Symbolic.S5 e197e1e
• Symbolic.Ki 9ac7e48
• reduce (symbolic) 8703f13
• add example to src/SMCDEL/Examples/ 7c92051
• quickcheck tests in tests/K.hs 0b76e2a

Before turning this draft into an actual pull request, Umberto, @BasLaa and I would like to ask:

• how the Ki module works overall; we see that all agents share an indexed BDD, for implementing bddOf for distributed knowledge, should we be setting the variables for all agents in a group to True?
• how we should approach testing (should we just run cabal test? How should we build knowledge structures with DD/CUDD to test with?).

Thanks!

P.S. We are also sending you our theoretical results via email. :)

[m4lvin]

Many thanks already for doing this!

• About Ki modules: @dushiel probably can answer it better than I can. I had a quick look at the thesis which very briefly discusses the idea of having one agent-indexed BDD instead of one BDD per agent. But I think it does not mention distributed knowledge.

  Setting all variables to true may give you dist-knowledge if the agent-indexed BDD was made with this usage in mind. Currently the assumption (I think, again @dushiel knows better) is that the agent-indexed BDD is only ever used with setting exactly one of the variables to true. So it may just return bottom (i.e. an empty relation) instead of the intersection. Or anything else actually 🤔

  Instead, maybe you want to compute a new BDD like this:
  

• Testing: Indeed there is a test suite. I usually use stack instead of cabal, and stack test --coverage also returns something like this.

  I guess many tests already will cover distributed knowledge because you added it here in the generation of random formulas 👍

  Most Examples are only defined for CacBDD, but you can look at SMCDEL.Examples.DiningCrypto.General and SMCDEL.Examples.SumAndProduct.General for CUDD examples. For DD there is only muddy children if I remember correctly.

  You can also add quickcheck tests to tests/Examples.hs, for example that on arbitrary models/structures common knowledge should imply distributed knowledge.

  CI is on GitLab so it does not run for your repository, but you should be able to run stack test or cabal test locally. The output of the test suite looks like this (and the CUDD tests tend to fail when running out of memory): https://gitlab.com/m4lvin/SMCDEL/-/pipelines

I will try to look at the code more later, overall it seems pretty tidy to me already :-)

[BasLaa]

Thanks for the review!

For the Ki modules: thanks for the suggestion, if setting all indexes to true doesn't give the result we want this is probably the way to go. The only thing is that it does might not be very fast to conjunct all the BDDs.

As a side note, I was wondering what the benefit is of the RelBDD type in Symbolic.K. Does the Tagged type with the empty datatype Dubbel indicate something? I believe it's for type safety, how does that work?

[foxyseta]

Still concerning tests:

• do we need to run tests that require installing/building graphviz, dot2tex, selenium/webdriver and such? These tools are not part of our current setups, but we could install them if you think said tests are relevant to distributed knowledge;
• I had to stop stack --no-terminal test --coverage smcdel:test:CUDD after 40 minutes of (non-parallel, intense) execution on my driver (next branch), but the Gitlab pipeline seems to be doing fine. On our own branch, my heap is exhausted (8192 MB). Could any of this be related to segmenation fault on mac M1 #35?

[m4lvin]

As a side note, I was wondering what the benefit is of the RelBDD type in Symbolic.K. Does the Tagged type with the empty datatype Dubbel indicate something? I believe it's for type safety, how does that work?

As a quick reply, see section 3.5 here: https://malv.in/phdthesis/gattinger-thesis.pdf#section.3.5 (page 98 middle onwards, mostly).

[m4lvin]

• do we need to run tests that require installing/building graphviz, dot2tex, selenium/webdriver and such? These tools are not part of our current setups, but we could install them if you think said tests are relevant to distributed knowledge;

No, I think there is nothing particular about distributed knowledge for these features. Once we merge this into next gitlab will run these things and if it breaks then we can fix it there before the next release.

• I had to stop stack --no-terminal test --coverage smcdel:test:CUDD after 40 minutes of (non-parallel, intense) execution on my driver (next branch), but the Gitlab pipeline seems to be doing fine. On our own branch, my heap is exhausted (8192 MB).

The CUDD tests are both memory-hungry and very non-deterministic, so please don't worry much about this. Also for Ki you may ignore / not test Ki_CUDD for now if it does not work.

Could any of this be related to segmenation fault on mac M1 #35?

I doubt it. Are you running on M1 or M2 hardware? Then I would actually be surprised if anything works because so far #35 prevented us (well, mostly @yukiniu) from evaluating anything involving (Has)CacBDD. I don't use any 🍎 stuff myself, so I can/did not investigate it further.

[dushiel]

Hi all,

I am aware of the side effect that having indexed agent knowledge within the same BDD as the statelaw works well with distributed knowledge in some sense. After discussing it we decided to leave it out of my thesis, which was getting lengthy.

From the top of my hat, i think you can indeed set the index variables of all agents in a group to true:

-- the DD representing the agent knowledge index has var i set to true, and other vars are set to dont-care. 
p_agent_i = bddOf (PrpF (P i)) 
-- "adding" an agent's knowledge the state law would be like conjuction 
new_statelaw = prev_statelaw `con`  (p_agent_i `imp` omega_i)
-- for multiple agents
new_statelaw2 = prev_statelaw `con`  (p_agent_i `imp` omega_i) `con`  (p_agent_j `imp` omega_j)
-- then we also have that
new_statelaw2 `imp` ((p_agent_i `con` p_agent_j ) `imp` (omega_i `con` omega_j)) == top
-- where (omega_i `con` omega_j) is what i think you mean with their distributed knowledge? 

Although i would still test/check it, there might be some combinations (e.g. action model update on ZDDs? ) that currently do not conserve the distributed knowledge. Its hard to remember exactly, if i find some spare time i can look into it.

I hope this clarifies a bit! Let me know if you have any more questions.

[foxyseta]

I doubt it. Are you running on M1 or M2 hardware? Then I would actually be surprised if anything works because so far #35 prevented us (well, mostly @yukiniu) from evaluating anything involving (Has)CacBDD. I don't use any 🍎 stuff myself, so I can/did not investigate it further.

I am actually on a Thinkpad. Segfaults would indicate a memory management/addressing bug in the underlying memory-unsafe code, so shouldn't they potentially bring about unexpected results on all machines? In my (limited) experience, Macintoshes are usually more prone to throwing segfaults in contrast to other unexpected behaviors, when compared to other platforms. @BasLaa is on M1, but I believe he hasn't tested this out.

More importantly, I am glad to know there's no need for us to worry about these tests. Thanks!

Hi all,

I am aware of the side effect that having indexed agent knowledge within the same BDD as the statelaw works well with distributed knowledge in some sense. After discussing it we decided to leave it out of my thesis, which was getting lengthy.

From the top of my hat, i think you can indeed set the index variables of all agents in a group to true:

-- the DD representing the agent knowledge index has var i set to true, and other vars are set to dont-care. 
p_agent_i = bddOf (PrpF (P i)) 
-- "adding" an agent's knowledge the state law would be like conjuction 
new_statelaw = prev_statelaw `con`  (p_agent_i `imp` omega_i)
-- for multiple agents
new_statelaw2 = prev_statelaw `con`  (p_agent_i `imp` omega_i) `con`  (p_agent_j `imp` omega_j)
-- then we also have that
new_statelaw2 `imp` ((p_agent_i `con` p_agent_j ) `imp` (omega_i `con` omega_j)) == top
-- where (omega_i `con` omega_j) is what i think you mean with their distributed knowledge? 

Although i would still test/check it, there might be some combinations (e.g. action model update on ZDDs? ) that currently do not conserve the distributed knowledge. Its hard to remember exactly, if i find some spare time i can look into it.

I hope this clarifies a bit! Let me know if you have any more questions.

Thanks for the detailed answer! We are actually not concerning ourselves with the state law itself, though. As for now, we would be just interested in retrieving the conjunction of a group of agent's observable laws. Hence, we would like to know if the general inequality @m4lvin depicted in the picture above is actually an equality for your specific implementation or not. If it is, even if it is probably an implementation detail, it could be turned into a feature by simply documenting it. If it doesn't, we could retrieve the observable laws one by one and then compute their disjunction.

[dushiel]

Ah, my apologies, i could have explained it better. I looked it up and the K operator is mainly defined by the line:

result = forallSet ps' <$> (imp <$> cpBdd (M.size ags) lawbdd <*> (imp <$> omegai <*> cpBdd (M.size ags) (bddOf bls form)))
-- this reflects: Forall paths through statelaw: statelaw -> (p_agent_i -> omega_i)
-- although, confusingly, the naming in the code is:
--    p_agent_i = omegai
--    omega_i = form
--    lawbdd = statelaw

So i am confident "getting" distributed knowledge is equal to setting the indexes of the agents in question to true. Testing it never hurts though. I set the index to true for an agent i with the line:

omegai = Tagged $ restrict (untag obdds) (ags ! i, True)

replacing restrict for restrictSet and i with [0..(M.size ags)] or something in that direction should be an implementation of distributed knowledge in Ki.

[foxyseta]

Thanks you so much! The namings initally threw me off.

[m4lvin]

Thanks for weighing in @dushiel!

I tried to find an actual example in code of a Ki structure, and I think this is the only one we have atm:

SMCDEL/test/CUDD.hs

Lines 221 to 230 in 80fa7bf

	myBlSKi :: (DdCtx a b c) => MyHaskCUDD.Manager -> Ki_CUDD.BelStruct a b c
	myBlSKi mgr = Ki_CUDD.BlS mgr defaultVocabulary (S5_CUDD.boolDdOf mgr Top) myObs where
	myObs :: (DdCtx a b c) => (M.Map Agent Int, Ki_CUDD.RelDD a b c)
	myObs = (M.fromList [("1", 0), ("2", 1), ("3", 2), ("4", 3), ("5", 4)], pure $ S5_CUDD.boolDdOf mgr $ Conj
	[ Impl (PrpF $ P 0) (Conj (zipWith Equi (map PrpF [P 5, P 7, P 9, P 11]) (map PrpF [P 6, P 8, P 10, P 12])))
	, Impl (PrpF $ P 1) (Conj (zipWith Equi (map PrpF [P 5, P 7]) (map PrpF [P 6, P 8])))
	, Impl (PrpF $ P 2) Bot
	, Impl (PrpF $ P 3) (PrpF $ P 5)
	, Impl (PrpF $ P 4) Top
	])

And indeed here we can get the distributed knowledge relation for a group using restrictSet as discussed.

What I think should be noted somewhere is that this only works if (here: because) the agent-indexed BDD does not give any restrictions on the variables used for indexing among each other. Concretely, if we would add something like "exactly one of {0,1,2,3,4,5} is true" to the Conj above then this would not affect the individual relations of all agents, but it would result in an empty relation for any group of two or more agents if we use the restrictSet method, while the (inefficient) "conjunction over all group members" method should still work then.

All that said, there may even be an automated way that from a possibly (by internal dependencies between the agent-indexing variables) broken BDD we can compute a proper BDD for which the restrictSet method works 🤔 But this is getting outside the scope of this PR I guess ;-)

I'll open separate issues for (i) the CUDD tests failing or OOMing and (ii) better testing of Ki with more examples.

[foxyseta]

Here's a sample txt:
https://codeberg.org/foxy/smcdel/src/branch/feat/dst-knw/Examples/MuddyChildrenDistributed.smcdel.txt
Here we are checking for some validities using QuickCheck: 0b76e2a

[foxyseta]

Perhaps the .smcdel.txt is not needed after all? I would not add it to smcdel-web personally. It could be either merged within the original MuddyChildren or removed altogether.

[m4lvin]

Indeed it would suffice to include an example formula with D in the existing MuddyChildren.smcdel.txt I would say too.

Overall, it looks good to me and ready to merge. Or did you still want to do other things?

[foxyseta]

The three of us are satisfied. Let us know if you would rather have us merge MuddyChildrenDistributed.smcdel.txt in MuddyChildren.smcdel.txt before accepting the PR.

[m4lvin]

Thank you!!