git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6593 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6590 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6589 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6588 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6587 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

updated GUI to generalize the typecheck procedure, default prover is now CVC, although this can be changed, currently not saved to the block, so each time you open it will go back to CVC, may want to change this in the future. need to fix some stuff in validation report

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6562 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

no longer runs COUNTERMODEL everytime, actually didn't even need to do the running twice idea as dissucessed earlier, actually a command line flag +model, that will automatically display the countermodel for na invalid query.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6561 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6560 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

added support for dependant subtypes, seems to work well with ones like the power conditioning example, if you try to give a specific type, ie. {x:real|x>5}, cvc is not able to prove unless you provide a witness of the type. Currently translates from pvs style typing to the cvc style so that user only needs to know one way, the pvs way is cleaner

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6559 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6558 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6556 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6525 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6524 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6523 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6521 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6520 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

begnining of application of SMT solver, using CVC3 solver. only works for 1D vertical grids right now, although easy to add more dimensions, etc. ALOT faster than PVS.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6519 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6360 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6352 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6351 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6319 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

have a mode working where tool will generate a theory using the simulink types, as well as an constraints expressed in the pvs types. for example if input is x:real, but in simulink diagram input is int8, will create a theory where input is of type int8, copies a pvs theory of the types to the pwd, currently using integer subranges for types, and real for floating pt types, not sure if I should use IEEE754, might lose test case generation with this. Typechecker forces proving that no over/under flow for outputs, this is not always automatic, and grind seems to have trouble with it sometimes.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6318 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

can now figure out compiled types of code block, could now use these types for proving, still need a way of consolidating types between input box and port definitions

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6317 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6314 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

fixed validation report so that it will properly interpret counter examples for enumerated pvs types, previously it would give error, now properly displays in window and highlights cells in main table

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6311 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6249 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6246 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6240 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

edited code looking for unsuppressed output, need better way to do this, also removed the check system block from the block library, it still needs some work

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6239 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6231 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6228 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6227 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6214 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6210 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

y

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6209 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

latest update, undo manager working better, need to implement redo for a few senarios, and fix undo when deleting the last remaining cell in a grid

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6207 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6200 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6199 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6164 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6163 57e6efec-57d4-0310-aeb1-a6c144bb1a8b