search

jrclogic / SMCDEL

A symbolic model checker for Dynamic Epistemic Logic.
https://w4eg.de/malvin/illc/smcdelweb
GNU General Public License v2.0
41 stars 9 forks source link

User-oriented documentation #43

Open RutaTang opened 6 months ago

RutaTang commented 6 months ago

Hi,

Do we have user-oriented documentation that could make it easier for beginners to understand the whole syntax of the input code of SMCDEL?

m4lvin commented 6 months ago

Hi, thanks for opening the issue!

I am afraid that at the moment there is no documentation for the input syntax used in the cli and web interfaces. The best we have are the Examples.

See also https://github.com/jrclogic/SMCDEL/issues/13 but we can leave this issue here open too, because not only the grammar but a general more "manual" like introduction would be good to have.

RutaTang commented 5 months ago

Before the manual comes out, may I double-check what is:

  1. LAW Top: "LAW" and "Top"?
  2. VARS 1,2: "1" can be considered as a proposition whose truth is not yet known right?

Really appreciate it if you can just give some brief explanations about it.

m4lvin commented 5 months ago

Here is a quick reply, let me know if this helps :-)

The first part of the input describes a knowledge structure:

VARS ...

LAW ...

OBS ...

It is best to also think about them in this order, so VARS first, then LAW.

VARS is the keyword before the vocabulary, i.e. the set of all atomic propositions. For example, when we write VARS 0,1 then this says in this structure we have two atomic propositions. One might also want to call them p,q but in SMCDEL currently all variables must be named by integers. Indeed in general the agents do not (yet) know the values of these propositions.

LAW is the keyword before a Boolean formula to say what states should exist. LAW Top says the constant true formula that says that all possible states should be there. So in our example we would have four states {}, {0}, {1}, {0,1}. Alternative we could say LAW 1 | 2 which would restrict this to three states {0}, {1}, {0,1}. All the variables/numbers used in this formula must be mentioned in VARS. All agents will know this formula, it is common knowledge.

OBS is the keyword before a map that then says which agent observes which of the atomic propositions. so a : 1,2 here means agent "a" observes variables 1 and 2. All variables mentioned in OBS must also be in VARS.

RutaTang commented 5 months ago

Very helpful! Thank you!!