K-user mailing list

[Lucas Pena <lpena7 AT illinois.edu>]

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

lpena7 AT illinois.edu

(954) 882-7070

--

Lucas Peña

University of Illinois at Urbana-Champaign

lpena7 AT illinois.edu

(954) 882-7070