# Formulae

```
<impl> ::= <disj> '=>' <impl> | <disj>
<disj> ::= <conj> '|' <disj> | <conj>
<conj> ::= <lit> '&' <conj> | <lit>
<mod>  ::= K1 | K2 | K3 | ... | K123 | ...
<lit>  ::= '!' <lit> | <mod> <lit> | <atom>
<alphanum> ::= (a-z_)(a-z_0-9)*
<atom> ::= <alphanum> | '(' <impl> ')'
```

Implicitly, consume an arbitrary number of whitespaces after every symbol.

e.g. `(asdf1=>b|K1K2asdf1) => K2asdf1 => asdf1&b`


# Structures

```
[n: number of primitive propositions] '\n'
n times: <alphanum> '\n'
[m: number of worlds] '\n'
m times: <alphanum> ':' (' ' <alphanum>)* '\n'
[k: number of relations] '\n'
for i from 1 to k: {
	'Ki' ':' '\n'
	m times: <alphanum> '~' (' ' <alphanum>)* '\n'
}
```

We first enumerate all the names of primitive propositions (lowercase alphanumeric strings not starting with a number). Then, we enumerate the worlds, and list the primitive propositions that are true at each of them. Finally, we enumerate the relations, and for each of them, list what they relate each world to.

You may assume that names of propositions and worlds are all unique, and no enumeration/list will contain redundant information. You should NOT assume that relations are in fact equivalence relations.

We may later extend these grammars to include relations that have names that do not adhere to the Ki scheme, such as T or Wi, and represent other concepts such as time or write permissions.

### Example:

struct1.txt:
```
3
asdf1
b
magic
5
w1: asdf13 b
w2: b asdf13
w3: magic
w4: magic asdf13
w5: magic asdf13 b
2
K1:
w1 ~ w1 w2 w4 w5
w3 ~ w3
w2 ~ w1 w2 w4 w5
w4 ~ w2 w4 w1 w5
w5 ~ w1 w2 w4 w5
K2:
w2 ~ w2
w1 ~ w1
w3 ~ w3 w4 w5
w4 ~ w3 w4 w5
w5 ~ w3 w4 w5
```

# Judgement inputs

Your model checker should accept two filenames: one structure description as above,
and one file that contains a list of judgements, one per line, of the form

```
<alphanum> '|=' <impl>
```
.

For example,

formulas1.txt:
```
w1 |= K1asdf13
w2 |= K1magic
w2 |= K2magic
w4 |= K1magic
w4 |= K2magic
w1 |= !K1!K2magic
w1 |= K1(b  |  K2 magic)
w1 |= K1( (b => !K2 magic) & (!K2magic => b) )
w3 |= K2(K1(K2magic | K2!magic))
```

Assuming the structure and the judgements were parsed successfully, the model checker
should evaluate each formula at the respective world, and output a line containing the string "True" if the judgement was true asnd "False" otherwise.

For the above examples, the model checker, when called as
`./modelchecker struct1.txt formulas1.txt`,
should output:

```
True
False
False
False
True
True
True
False
True
```