-
Notifications
You must be signed in to change notification settings - Fork 61
K Wish List
This page is a list of features that K users wish K to have...
(Currently threads are sorted by alphabetical order of the contents of the the first cells in it, usually K cell, but users might want it to be ordered differently)
- Dwight: If the thread ID cell is placed before the K cell within the thread cell, it should sort alphabetically by the thread ID.
- Grigore: It would be good eventually to allow people to reorder the solutions based on various options they care about, without having to modify the configuration.
LTL model checking: is it mandatory to change the syntax to include labels and to define equality functions and other atomic propositions
- Dorel: The LTL model checker (that used in Cink) works only with the Maude backend (no longer available in the last version). Generally, the property language (here the language for atomic propositions) is distinct from the programming language. In oder to check the properties, you need both languages. Moreover, the satisfaction relation between configurations and the atomic propositions must be defined. The satisfaction relation is given as C |=Ltl At and says that the atomic proposition At holds for the configuration C (it is the labelling function in terms of Kripke structures).( _ |=Ltl _ is implemented as a function Bag X Prop -> Bool .) These two components MUST be sent to the Maude LTL model-checker by the backend tool. But no need to change configuration. In my opinion, these two components are required by any LTL model-checker built for K definitions. The labels are required only if you want to have an atomic proposition saying "the execution of the program reached the statement with the label L".
Rules with precedence: To be able to give one rule more precedence than another, so that if both rules match, the one with higher precedence is executed.
- Cosmin: Assigned to.
Currently we can pass in this value with krun -cVARNAME=Value, but it would be good to be able to set a default value to it inside the k file so that if I do only krun, it would use the default value, but if I do krun -cVAR=v, then v would overwrite the default value.
-
Andrei Arusoaie: proposed to have a 'default' attribute in the configuration for setting the default value
-
Radu: $A ~> $B how can I specify the default for both? How about default($A:Sort, 'some term here') ~> default($B:Sort2, 'some other term') I don't like the idea of putting the default value for a variable in the list of attributes for a cell. Considering separation of concerns, I don't see the connection between the two. That's why I'm proposing this special term with special semantics at the krun level.
Add strict kompilation mode so that all the inferred sorts for all the variables that appear in all rules are checked at runtime.
https://github.com/kframework/k/issues/1399
There are many people who prefer to define languages purely syntactically, that is, where each term that appears at any moment during the application of their rules parse correctly according to their defined grammar. For such people, allowing a term of a certain sort on a position where a different sort is expected during rewriting indicates a serious problem, one that they would like to be aware of.
- Grigore: I therefore propose a strict kompilation mode, where all the inferred sorts for all the variables that appear in all rules are checked at runtime. We may go even further with this, and have a kompiler step which adds these runtime checks to any K definition, based entirely on the declared sorts in the productions corresponding to
###Add versioning to kserver #1867 When kserver is called from kompile or krun, version info should be exchanged as part of the protocol to ensure no inconsistencies between the two. This is useful for devs with multiple versions of K, users who are upgrading between versions of RV-Match, etc. The current latest commit hash can be used as in the version message.