projects / cdsspec-compiler.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8da693d) | patch
nodestack: push 'create_cv' functionality responsibility back to ModelChecker
authorBrian Norris <banorris@uci.edu>
Tue, 29 May 2012 17:46:42 +0000 (10:46 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 29 May 2012 21:39:22 +0000 (14:39 -0700)
commit9397658596cfa29f81242b5f06e80d1d9cdf6d14
treeb360d45b7384d7ba574f267866f151e7e1535ef7tree | snapshot
parent8da693d1a0d03aeba127f434c84fcb372314b93acommit | diff
nodestack: push 'create_cv' functionality responsibility back to ModelChecker

It doesn't really make sense to have NodeStack call the 'create_cv' function
for a ModelAction. This commit separates the functionality of 'explore_action'
from 'create_cv', calling each separately from the higher-level
'check_current_action' model-checking function.
action.cc diff | blob | history
model.cc diff | blob | history
nodestack.cc diff | blob | history
nodestack.h diff | blob | history
This is the public repository for the CDSSpec specification compiler.