k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

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

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

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