Feature requests from logic classmates peer feedback

[vezwork]

In order of priority:

P1

• written instructions for use
• the operator “everyone,” as in Ea,b,etc. OR K[a,b] used for group knowledge. One could consider this very important, since for example the homework question where this playground could be most useful would be homework 6 question 1, where we were asked to disprove Ea,b A -> KaKb A
• public announcement logic either as formulas or as buttons you can press to "announce" something and change the model.

P2

• Pre-made examples It might also be helpful to have some pre-loaded example models. In fact, these pre-loaded models could potentially demonstrate certain frame correspondences that hold such as K, T, 4, 5. This would not only help new users, but would demonstrate why certain frame correspondences hold by way of some visual examples.
• instructional video attaching a video on your webpage showing how you illustrate an argument using your playground, just to give the new player better instruction?

P3

• Sequential World Numbers once a world is deleted and a new world is added, the numbers are not necessarily sequential. This in-turn can make the labels on the worlds confusing. Alternatively it might be good to give users the option to name each world.
• Agent Arrow editing UI When an agent arrow is selected, it seems odd that a keyboard shortcut is needed to change direction. Adding a small panel to change the arrow direction under the agent and variable selectors may make this more clear.
• Common Knowledge Operator from definition 15.6 in the course text. This seems difficult to do correctly since it involves infinity. I'm sure it's possible for finite models, but not easy.
• Code Cleanup & Documentation The current code files are long and disorganized, organize the code, add inline documentation, and add documentation to the github page so other people can contribute or understand the project.