Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Amusement is now a major application domain of computers and entertainment software has a certain degree of importance to consumers. The target of this thesis is entertainment software with interactive stories that dynamically branch according to users' actions. Script languages for describing such scenarios usually tend to be rather _ad hoc_ and naive, which often leads to bugs in those scenarios. This thesis proposes a scenario description language with clear and simple syntax and semantics, which enables systematic verification of consistency conditions of complex scenarios. The language is based on a state transition model with a finite number of variables varying over a finite number of values, where a scenario is described as a set of commands that (1) are guarded by conditions over the value of variables, (2) may branch over user input, and (3) modify the value of variables. Our automatic scenario checker traces every possibility of the user input in parallel. Since this parallelism is highly fine-grained, the checker makes use of StackThreads, a generic library for fine-grained multi-threading. It also exploits shortcuts and confluence found in a given scenario in order to reduce the number of states to explore.