Disprover unable to type variables of refined machines
Description
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
Details
Assignee

Reporter

Priority
More fields
Story Points, Original estimate
More fields
Story Points, Original estimateCreated March 27, 2013 at 5:40 PM
Updated March 28, 2013 at 10:23 AM
Resolved March 28, 2013 at 10:23 AM
Variables contained in refined machines are detected as global sets. Examples will follow tomorrow.