Re:Introduction to TLA+ Model Checking in the Command Line
by mcguire on Friday January 18, 2019 @10:56AM
(#18940123)
Normal testing feeds selected inputs to the software and succeeds for the corresponding output.
QuickCheck feeds random values to the software and looks for "good" results.
TLA+ takes a model of the system (not the software) and explores the entire state space and looks for anything that violates given logical predicates. It is a different later of abstraction.
QuickCheck feeds random values to the software and looks for "good" results.
TLA+ takes a model of the system (not the software) and explores the entire state space and looks for anything that violates given logical predicates. It is a different later of abstraction.