search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Is krun --graph working? #1152

Open osa1 opened 9 years ago

osa1 commented 9 years ago

krun --search --graph is not tested at all. I recently fixed a bug about it(#1151). After fixing the exceptions I tried to run some examples but none of them printed anything extra to --search. I was wondering if that feature is working.

It'd be nice to add some meaningful tests about this feature because otherwise it'll get broken again. Can anyone explain why it's not doing anything different than --search currently?

(Tried with Java backend too, got same results. e.g. worked exactly same as only --search)

grosu commented 9 years ago

Mansavi, can you please chip in here? BTW, I just noticed that you are NOT a member of the K team on github. How comes, after all this time? Please send me your github ID to add you.

Here is a radical thought. If you think we should not do that, please jump with your feet on this proposal and kill it before it grows (I'm CC-ing the k-list, to make sure nobody misses this message):

Let us get rid of the Maude backend from the K kernel (or just Kernel?)!

Let's make it a module, and then let the people interested in it maintain it. We will soon have no benefit from having a Maude backend, so all this maintenance effort we put into the Maude backend is little justified. Instead, we can go full throttle with the Java backend and a super-duper debugger for it, with graph output capabilities as we want them to be, and not as Maude give them to us. Those language definitions that are still stuck with Maude can simply require a certain release of K (of course, if we go with the above then we should release first).

Grigore

From: Ömer Sinan Aðacan [notifications@github.com] Sent: Tuesday, November 04, 2014 5:40 AM To: kframework/k Subject: [k] Is krun --graph working? (#1152)

krun --search --graph is not tested at all. I recently fixed a bug about it(#1151https://github.com/kframework/k/pull/1151). After fixing the exceptions I tried to run some examples but none of them printed anything extra to --search. I was wondering if that feature is working.

It'd be nice to add some meaningful tests about this feature because otherwise it'll get broken again. Can anyone explain why it's not doing anything different than --search currently?

(Tried with Java backend too, got same results. e.g. worked exactly same as only --search)

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/1152.

grosu commented 9 years ago

If I remember corectly, the idea was to have an API for Krun, backend-independent.

Ideally, this would mean KRun would produce terms, pairs of terms, tuples of terms and rules, depending on what it is asked to do (reduce, trace, find path to a loop in model checking, and so on). If this is the case, and if KRun can, for example given a term to produce all terms reachable in one (or more steps), with annotations about the rules applied, then writing a debugger should be backend-independent.

I agree that the current debugger depends on Maude, but this is due to the fact that there was no clean and clear interface in KRun which would allow it to be backend-independent. Moreover, if I remember correctly, the current debugger does some of the things the Maude backend Krun should have done, i.e., converting from Maude output to KIL (to be KORE) terms.

Making the debugger a backend-independent module would help standardize the KRun interface, and would benefit any backend, not just one (though it should be much faster for the Java one as it would require less conversions).

Traian

2014-11-04 13:56 GMT+02:00 Rosu, Grigore grosu@illinois.edu:

Mansavi, can you please chip in here? BTW, I just noticed that you are NOT a member of the K team on github. How comes, after all this time? Please send me your github ID to add you.

Here is a radical thought. If you think we should not do that, please jump with your feet on this proposal and kill it before it grows (I'm CC-ing the k-list, to make sure nobody misses this message):

 Let us get rid of the Maude backend from the K kernel (or just

Kernel?)!

Let's make it a module, and then let the people interested in it maintain it. We will soon have no benefit from having a Maude backend, so all this maintenance effort we put into the Maude backend is little justified. Instead, we can go full throttle with the Java backend and a super-duper debugger for it, with graph output capabilities as we want them to be, and not as Maude give them to us. Those language definitions that are still stuck with Maude can simply require a certain release of K (of course, if we go with the above then we should release first).

Grigore

From: Ömer Sinan Ağacan [notifications@github.com] Sent: Tuesday, November 04, 2014 5:40 AM To: kframework/k Subject: [k] Is krun --graph working? (#1152)

krun --search --graph is not tested at all. I recently fixed a bug about it(#1151 https://github.com/kframework/k/pull/1151). After fixing the exceptions I tried to run some examples but none of them printed anything extra to --search. I was wondering if that feature is working.

It'd be nice to add some meaningful tests about this feature because otherwise it'll get broken again. Can anyone explain why it's not doing anything different than --search currently?

(Tried with Java backend too, got same results. e.g. worked exactly same as only --search)

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/1152.

k-list mailing list k-list@cs.uiuc.edu http://lists.cs.uiuc.edu/mailman/listinfo/k-list

grosu commented 9 years ago

The debugger is definitely going to be backend-independent! However, in order to transit to the Krun API, we need to refactor lots of code, including the code in the Maude backend. While keeping the Maude backend would give us more confidence that we are backend independent, this actually slows us a lot. Those of you doing refactoring, please let us know if this claim is incorrect. So my proposal is to extract the Maude backend into a separate module, and not worry about it during the rafactoring. Then, once the Krun/K API is available, those interested in the Maude backend should have an easy job to make it work with the new Kernel.

Grigore

From: traian.serbanuta@gmail.com [traian.serbanuta@gmail.com] on behalf of Traian Florin Şerbănuţă [traian.serbanuta@fmi.unibuc.ro] Sent: Tuesday, November 04, 2014 7:15 AM To: Rosu, Grigore Cc: kframework/k; k-list@cs.illinois.edu Subject: Re: [k-list] [k] Is krun --graph working? (#1152)

If I remember corectly, the idea was to have an API for Krun, backend-independent.

Ideally, this would mean KRun would produce terms, pairs of terms, tuples of terms and rules, depending on what it is asked to do (reduce, trace, find path to a loop in model checking, and so on). If this is the case, and if KRun can, for example given a term to produce all terms reachable in one (or more steps), with annotations about the rules applied, then writing a debugger should be backend-independent.

I agree that the current debugger depends on Maude, but this is due to the fact that there was no clean and clear interface in KRun which would allow it to be backend-independent. Moreover, if I remember correctly, the current debugger does some of the things the Maude backend Krun should have done, i.e., converting from Maude output to KIL (to be KORE) terms.

Making the debugger a backend-independent module would help standardize the KRun interface, and would benefit any backend, not just one (though it should be much faster for the Java one as it would require less conversions).

Traian

2014-11-04 13:56 GMT+02:00 Rosu, Grigore grosu@illinois.edu<mailto:grosu@illinois.edu>: Mansavi, can you please chip in here? BTW, I just noticed that you are NOT a member of the K team on github. How comes, after all this time? Please send me your github ID to add you.

Here is a radical thought. If you think we should not do that, please jump with your feet on this proposal and kill it before it grows (I'm CC-ing the k-list, to make sure nobody misses this message):

Let us get rid of the Maude backend from the K kernel (or just Kernel?)!

Let's make it a module, and then let the people interested in it maintain it. We will soon have no benefit from having a Maude backend, so all this maintenance effort we put into the Maude backend is little justified. Instead, we can go full throttle with the Java backend and a super-duper debugger for it, with graph output capabilities as we want them to be, and not as Maude give them to us. Those language definitions that are still stuck with Maude can simply require a certain release of K (of course, if we go with the above then we should release first).

Grigore

From: Ömer Sinan Ağacan [notifications@github.commailto:notifications@github.com] Sent: Tuesday, November 04, 2014 5:40 AM To: kframework/k Subject: [k] Is krun --graph working? (#1152)

krun --search --graph is not tested at all. I recently fixed a bug about it(#1151https://github.com/kframework/k/pull/1151). After fixing the exceptions I tried to run some examples but none of them printed anything extra to --search. I was wondering if that feature is working.

It'd be nice to add some meaningful tests about this feature because otherwise it'll get broken again. Can anyone explain why it's not doing anything different than --search currently?

(Tried with Java backend too, got same results. e.g. worked exactly same as only --search)

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/1152.

k-list mailing list k-list@cs.uiuc.edumailto:k-list@cs.uiuc.edu http://lists.cs.uiuc.edu/mailman/listinfo/k-list