% $Id: Configuration.oz,v 1.11 2010/01/31 21:57:41 leavens Exp leavens $ % Configurations (States) % AUTHOR: Gary T. Leavens % Representation: % ::= state( > ) | msg() %% In a state(N Ths Sto), N is the index of the selected thread (from Ths) %% and 0 =< N =< {Length Ths}, with 0 meaning no thread is selected. % ::= runnable() | suspended( ) % ::= #> \insert 'Store.oz' \insert 'Unparse.oz' declare fun {InputToConfig Stmt} %% ENSURES: Result is an initial configuration containing Stmt %% where the initial environment and store are empty {MakeConfig Stmt {InitEnv} {EmptyStore}} end fun {MakeConfig Stmt Env Store} %% ENSURES: Result is an initial configuration containing Stmt %% and the given environment and store state(1 [runnable(Stmt#Env|nil)] Store) end fun {SingleThreadConfig Thread Store} %% ENSURES: Result is a configuration containing the given thread and store %% with a run index of 1. state(1 Thread|nil Store) end fun {IsTerminalConfig Config} %% ENSURES: Result is true when the configuration is terminal case Config of state(_ Threads _) then {All Threads IsTerminalThread} else true end end fun {IsTerminalThread Thread} %% ENSURES: Result is true when the thread is terminated case Thread of runnable(nil) then true else false end end fun {IsRunnableThread Thread} %% ENSURES: Result is true when the thread is terminated case Thread of runnable(_) then true else false end end fun {IsSuspendedThread Thread} %% ENSURES: Result is true when the thread is terminated case Thread of suspended(...) then true else false end end fun {CanProgress Config} case Config of state(_ Threads _) then {Some Threads IsRunnableThread} else false end end fun {Output Config} %% REQUIRES: Config is terminal %% ENSURES: Result is the output of Config (a store or message) case Config of state(_ _ Store) then Store [] msg(Message) then Message else raise cantOutputFromNonTerminalConfig end end end fun {RunIndexOfConfig state(N _ _)} %% ENSURES: Result is index of the process to run from a config. N end fun {ThreadsOfConfig state(_ Threads _)} %% ENSURES: Result is the list of threads from a config Threads end fun {StoreOfConfig state(_ _ Store)} %% ENSURES: Result is the store of a normal config Store end fun {SelectedThreadOfConfig state(N Threads _)} {Nth Threads N} end fun {IncWrapping N Len} %% ENSURES: result is N+1 wrapping back to 1 if the result reaches Len+1 NewN = N+1 in if NewN > Len then 1 else NewN end end fun {NextRunnable state(N Threads Sto)} %% REQUIRES: One of the threads in Threads is runnable. %% ENSURES: Result is a state that is like the argument, %% but where the selected thread index is moved to %% the next runnable thread number. NewN = {IncWrapping N {Length Threads}} Next = state(NewN Threads Sto) in if {IsRunnableThread {Nth Threads NewN}} then Next else {NextRunnable Next} end end fun {Replace Lst E N} %% REQUIRES: Lst has at least N elements %% ENSURES: Result is the same as Lst, but with the Nth element relplaced by E. {Append {List.take Lst N-1} E|{List.drop Lst N}} end fun {ReplaceThread state(Index Threads Store) N NewThread} %% REQUIRES: 1 =< N and N =< {Length Threads} %% ENSURES: Result is the same state as the argument, %% but with the Nth thread replaced by NewThread state(Index {Replace Threads NewThread N} Store) end fun {ReplaceThreadAndStore state(Index Threads _) N NewThread NewStore} %% REQUIRES: 1 =< N and N =< {Length Threads} %% ENSURES: Result is the same state as the argument configuration, %% but with the Nth thread replaced by NewThread %% and the store replaced by NewStore state(Index {Replace Threads NewThread N} NewStore) end fun {StackOfThread Thread} %% ENSURES: Result is the stack from a single-threaded state case Thread of runnable(Stack) then Stack [] suspended(Stack) then Stack end end fun {WaitingOn suspended(_ Loc)} %% ENSURES: Result is the location this suspended thread is waiting on Loc end fun {EqualThreads Thread1 Thread2} %% ENSURES: Result is true if Thread1 is equivalent to Thread2 case Thread1#Thread2 of runnable(nil)#runnable(nil) then true [] runnable(Stmt1#Env1|Rest1)#runnable(Stmt2#Env2|Rest2) then Stmt1 == Stmt2 andthen {EqualEnv Env1 Env2} andthen {EqualThreads runnable(Rest1) runnable(Rest2)} [] suspended(Stmt1#Env1|Rest1 Loc1)#suspended(Stmt2#Env2|Rest2 Loc2) then Stmt1 == Stmt2 andthen {EqualEnv Env1 Env2} andthen {EqualThreads runnable(Rest1) runnable(Rest2)} else false end end fun {EqualThreadLists Threads1 Threads2} %% ENSURES: Result is true iff the two lists of threads are equal. case Threads1#Threads2 of nil#nil then true [] (Thrd1|Rest1)#(Thrd2|Rest2) then {EqualThreads Thrd1 Thrd2} andthen {EqualThreadLists Rest1 Rest2} end end fun {EqualConfig C1 C2} %% ENSURES: Result is true if the two configurations are equal case C1#C2 of state(_ Threads1 Store1)#state(_ Threads2 Store2) then {EqualStore Store1 Store2} andthen {EqualThreadLists Threads1 Threads2} [] msg(M1)#msg(M2) then M1 == M2 else false end end fun {StringForStack Stack} %% ENSURES: Result is a virtual string representing the Stack argument case Stack of nil then 'n'#'il' [] (Stmt#Env)|Rest then '('#{Unparse Stmt}#', '#{StringForEnv Env}#')' # '|' # {StringForStack Rest} end end fun {StringForThread Thread} case Thread of runnable(Stack) then 'runnable('#{StringForStack Stack}#')' [] suspended(Stack Loc) then 'suspended('#{StringForStack Stack}#' waitingOn:'#{NameLoc Loc}#')' end end fun {StringForThreadsRest Rest} %% ENSURES: Result is a virtual string representing the Rest argument case Rest of nil then nil [] Thd|Rest then ', '#{StringForThread Thd}#{StringForThreadsRest Rest} end end fun {StringForThreads Threads} %% ENSURES: Result is a virtual string representing the Threads argument case Threads of nil then 'n'#'il' [] Thd|Rest then '{'#{StringForThread Thd}#{StringForThreadsRest Rest}#'}' end end fun {StringForConfig C} %% ENSURES: Result is a virtual string representing C case C of state(N Threads Store) then '(' # {IntToString N} # ', ' # {StringForThreads Threads} # ', ' # {StringForStore Store} # ')' [] msg(Message) then 'failed('#Message#')' end end