Skip to Content.
Sympa Menu

k-user - Re: [[K-user] ] LTS from K

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] LTS from K


Chronological Thread 
  • From: Lucas Pena <lpena7 AT illinois.edu>
  • To: Omar Duhaiby <3omarz AT gmail.com>
  • Cc: "Pena, Lucas" <lpena7 AT illinois.edu>, "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
  • Subject: Re: [[K-user] ] LTS from K
  • Date: Mon, 6 Feb 2017 18:17:45 -0600

Unfortunately, there's no clean way to do that right now. However, in the future, we will have a way to do this with the debugger. For now, since to use "--search" you need to tag rules with "transition" (or use the "--transition" option) anyway, you can use this selectively in combination with iterative applications "--depth" option to help generate the sequence you need.

Please let me know if you have any other questions.

On Mon, Feb 6, 2017 at 5:53 PM, Omar Duhaiby <3omarz AT gmail.com> wrote:
Yes, exactly. I'm looking for the sequences of transitions specific to my input. And I'm not expecting a single path, because K explores multiple paths.

On 7 February 2017 at 00:39, Lucas Pena <lpena7 AT illinois.edu> wrote:
Hi Omar,

The labeled transition system K internally analyzes is your K definition. Are you looking for more of the specific sequences of transitions that are fired on a specific input?

On Mon, Feb 6, 2017 at 4:45 PM, Omar Duhaiby <3omarz AT gmail.com> wrote:
Hello,
When running "Krun --search" or "Krun --ltlmc", doesn't K internally analyze a labeled transition system that it has generated from the input source code? If so, can K output this transition system?
Sincerely,
Omar



--
Lucas Peña
University of Illinois at Urbana-Champaign




--
Lucas Peña
University of Illinois at Urbana-Champaign
(954) 882-7070



Archive powered by MHonArc 2.6.19.

Top of Page