hub / github.com/ModelInference/synoptic / refineCExample

Method refineCExample

csight/src/csight/main/CSightMain.java:1620–1688 · view source on GitHub ↗

Matches the sequence of events in the counter-example to paths of corresponding GFSM states for each process. Then, refines each process' paths until all paths for some process are successfully refined. @return Whether a refinement was performed. @throws Exception if we were not able to

(GFSM pGraph, MCcExample cexample)

Source from the content-addressed store, hash-verified

source not stored for this graph (policy: none)

Callers 3

checkInvsRefineGFSMMethod · 0.95

processUnsafeModelResultMethod · 0.95

checkMultipleInvsRefineGFSMMethod · 0.95

Calls 9

getNumProcessesMethod · 0.95

checkPathCompletenessMethod · 0.95

isAcceptMethod · 0.95

isInitialMethod · 0.95

getCExamplePathsMethod · 0.80

numEventsMethod · 0.80

lastStateMethod · 0.80

toStringMethod · 0.65

refineMethod · 0.45

Tested by

no test coverage detected