modes: Object reference not set to an instance of an object
The following model makes modes crash (copied from Arnd's thesis):
action flip, end, show_heads, show_tails, see_heads, see_tails;
action show_heads1, show_tails1, show_heads2, show_tails2, show_heads3, show_tails3;
const int N = 3;
int(0..N) pay, nagree;
bool done;
property Terminate = Pmax(<> done);
property Correct = Pmax(<> done && (nagree%2 == N%2 && pay == 0
|| nagree%2 != N%2 && pay != 0));
process Cryptographer(int(1..N) id) {
bool heads, agree;
process Show() {
alt {
:: when(heads) show_heads
:: when(!heads) show_tails
}
}
process See() {
alt {
:: see_heads {= agree = heads =}
:: see_tails {= agree = !heads =}
}
}
flip palt { :1: {= heads = true =} :1: {= heads = false =} };
par { :: Show() :: See() };
tau {= nagree += ((agree == (pay != id)) ? 1 : 0) =}; end
}
process Payment() {
// Choose a scenario probabilistically
flip {= pay = DiscreteUniform(0, N) =}; end {= done = true =}
}
par {
:: Payment()
:: relabel { show_heads, show_tails, see_heads, see_tails }
by { show_heads1, show_tails1, show_heads3, show_tails3 }
Cryptographer(1)
:: relabel { show_heads, show_tails, see_heads, see_tails }
by { show_heads2, show_tails2, show_heads1, show_tails1 }
Cryptographer(2)
:: relabel { show_heads, show_tails, see_heads, see_tails }
by { show_heads3, show_tails3, show_heads2, show_tails2 }
Cryptographer(3)
}
With the following output & error:
(00:00) 0......
Preparing simulation...
figure-4-16-dining-cryptographers.modest: info: figure-4-16-dining-cryptographers is an STA model and will be simulated as an SHA.
(00:00) 0..........
Checking for supported use of clocks and continuous variables...
figure-4-16-dining-cryptographers.modest: info: Using default value of 0.95 for the confidence parameter.
figure-4-16-dining-cryptographers.modest: info: Using default value of 0.01 for the absolute half-width parameter.
Unhandled Exception: System.NullReferenceException: Object reference not set to an instance of an object.
at Modest.Simulation.ProbabilisticReachabilityProperty.IsCompatible(Property property)
at Modest.Simulation.SimulationProperty.GetPropertyInfo(Property property)
at Modest.Simulation.SimulationAnalysisEngine.Analyze(AnalysisParams analysisParameters, NSHAModel model, OperationState operationState, IErrorHandler errors)
at Modest.Simulation.SimulationAnalysisEngine.Analyze(AnalysisParams analysisParameters, NSHAModel model, IEnumerable`1 modelParameters, OperationState operationState, IErrorHandler errors)
at Modest.Modularity.AnalysisEngine`3.Analyze(IParameterObject analysisParameters, IModel model, IEnumerable`1 experiments, OperationState operationState, IErrorHandler errors)
at Modest.Executables.Modes.Program.Run(ModesParams parameters, Stopwatch time)
at Modest.Executables.Modes.Program.Main(String[] args)