k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

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

From: Omar Duhaiby <3omarz AT gmail.com>
To: Lucas Pena <lpena7 AT illinois.edu>
Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Subject: Re: [[K-user] ] LTS from K
Date: Tue, 7 Feb 2017 00:53:04 +0100

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

[[K-user] ] LTS from K, Omar Duhaiby, 02/06/2017
- <Possible follow-up(s)>
- Re: [[K-user] ] LTS from K, Lucas Pena, 02/06/2017
  - Re: [[K-user] ] LTS from K, Omar Duhaiby, 02/06/2017
  - Message not available
    - Re: [[K-user] ] LTS from K, Lucas Pena, 02/06/2017