Pathemeous / Symbolic-Gossip

Symbolic Model Checker for the Gossip Problem
GNU General Public License v2.0
2 stars 0 forks source link

Create 'Explain' function to relate generated proposition numbers back to conceptual propositions #2

Closed Pathemeous closed 3 months ago

Pathemeous commented 4 months ago

Propositions generated have a semi-arbitrary numbering. It is not immediately obvious what each proposition stands for, making it hard to reason about the visualisations and output.

Pathemeous commented 4 months ago

Relevant comment made here by @mgignoux https://github.com/Pathemeous/Symbolic-Gossip/commit/25c2e8ab6c5ea5cb6d3079e956e8c1265bb607e3#commitcomment-142141516

I added a parameter for number of agents, so you can modulo that, but I think we need to change "thisCallProp" in Malvin's code because he uses 10, but we should change that 10 to the number of agents. So this code is not working yet because we also need to change Malvin's file. Or we can just assume <10 agents.

Pathemeous commented 4 months ago

Replying to @mgignoux: I think there are also propositions offset with 100. It seems that this ams to create disjoint sets (some in the 10-99 range, some in the 100+ range). Maybe that clarifies the use of 10 in the original codebase.

Zjoris commented 4 months ago

In what kind of format do we want the output of explanations? A string that given a call/secret/Knowledge structure, tells you what everything means? Or is it an option to create a new type secretProp :: S Int Int and CallProp :: Q Int Int that we can put into a knowledge structure. Or both? Haha

Zjoris commented 4 months ago

So Explain now works for the initial model. But when using doCall to do an update on the initial model the vocabulary gets a couple of propositions that I do not know how to interpret. Since we are going to use a different update that makes different proposition I will wait with the rest of explain until the new transformer is further specified.

m4lvin commented 4 months ago

Maybe this helps to clarify a bit: Indeed the 100.. is to ensure disjoint sets, but mostly for human readability. The update function also uses shiftPrepare from here to ensure V+ is disjoint from V before actually applying the transformer. In the case of the call transformer it actually shifts down 100 to max(V)+1, 101 to max(V)+2 etc.

As for the explain function, I think it should only explain the basic vocabulary who knows which secret, i.e. the original V, and not even try to explain the additionally added atoms after an update (which may also disappear again if you use optimize).

Pathemeous commented 3 months ago

Closed and completed.