k-legacy
k-legacy copied to clipboard
kframework
The K tools (deprecated, see README)
I'm using the online interface, definition 1_k/1_lambda/lesson_1. kompile then krun with arguments ``` free-variable-capture.lambda -d .. -pattern " V:K " ``` Getting this error message: ``` [Error] Critical: Dynamic parameter...
Hello, I want to use Z3 solver of the K tool in order to verify my models. where may I find documentations or examples?? Thank you for replying.
Sorry for an naive question. I try to understand what happens two or more rules are matched? do they all fired to give rise to different runs? For example, I...
Can you provide me syntax or semantics which take input from user in k in imp language?
The following was sent on k-list. Since I didn't receive an answer yet, I include it here for recording. I would like to write a rule of the form rule...
I will give you may files, but it doesn't accept .k files, so I have renamed then .txt files. [arith.txt](https://github.com/kframework/k/files/166406/arith.txt) [bool.txt](https://github.com/kframework/k/files/166407/bool.txt) [arithbool.txt](https://github.com/kframework/k/files/166408/arithbool.txt) [simp3.txt](https://github.com/kframework/k/files/166412/simp3.txt) [test.txt](https://github.com/kframework/k/files/166413/test.txt) # # stack trace below here...
kjkompile.sh Preprocessing semantics: [Error] Compiler: Could not find sorts: [SwitchLabel] Source(/home/harshita/java-semantics/src/./prep/../common/list-syntax.k) Location(36,38,36,95) Execution semantics: [Error] Critical: Could not find file: builtins/model-checker.k Lookup directories:[./exec, /home/harshita/new/k/lib/java/../../include/builtin] Source(/home/harshita/java-semantics/src/./exec/ltl-support.k) Location(1,1,1,34) still producing error
In a meeting with Ben yesterday, it came out that we can use narrowing for parsing. This morning I did some experiments using Maude's narrowing support to flush out the...
bash-3.2$ pwd /Users/elsa/courses/cs422/sp2016/students/_class/_private/lectures/5 bash-3.2$ ls -d int-kompiled/ int-kompiled/ bash-3.2$ ls test.int test.int bash-3.2$ krun --directory "/Users/elsa/courses/cs422/sp2016/students/_class/_private/lectures/5/int-kompiled/" test.int [Error] Critical: Could not find a compiled definition. Use --directory to specify one....
Very strange problem: ``` yuwen2@yuwen2-HP-Z220-CMT-Workstation:~/k/k-distribution/tutorial/1_k/5_types/lesson_1$ ktest tests/config.xml Running ['/home/yuwen2/k/k-distribution/target/release/k/bin/kompile' '/home/yuwen2/k/k-distribution/tutorial/1_k/5_types/lesson_1/imp.k'] Done with ['/home/yuwen2/k/k-distribution/target/release/k/bin/kompile' '/home/yuwen2/k/k-distribution/tutorial/1_k/5_types/lesson_1/imp.k'] ``` After I run the above ktest, krun right after that produced correct result; however, if...
