Skip to:

  1. Skip to Jira Navigation
  2. Skip to Side Navigation
  3. Skip to Main Content

Disprover unable to type variables of refined machines

Description

Variables contained in refined machines are detected as global sets. Examples will follow tomorrow.

Environment

None

Gliffy Diagrams

Activity

Show:

Sebastian Krings March 28, 2013 at 10:23 AM

Added known types of variables and constants to the type environment before type checking the sequent.

Sebastian Krings March 27, 2013 at 7:26 PM

Machine loading seams to be done correctly. However, type checking the sequent returns wrong types for variables of refined machines. These variables are not typed by the invariant, but rather by the invariant of the refined machine. We might need to include typing information from the abstract machines in the sequent predicate send to ProB.

Fixed

Details

Assignee

Reporter

Priority

More fields

Created March 27, 2013 at 5:40 PM
Updated March 28, 2013 at 10:23 AM
Resolved March 28, 2013 at 10:23 AM
Configure