曾经的笔记，看起来参考链接对理解SMC很有用，先都贴过来。

Verification Progress Dialog

The verification progress dialog displays 参考链接：UPPAAL web help](https://www.it.uu.se/research/group/darts/uppaal/help.php?file=Verifier/Verifying.shtml) )

1. the progress of how many queries have been verified
2. what is the current load of a passed-waiting list
3. current processor time usage ```

• blue: the time spent for verification
• red: the time spent by operating system ```

1. current usage of host’s random access memory ```

• blue: verification memory
• gray: memory used by other running processes
• yellow: operating system cache and buffers ```

1. swap disk usage ```

• blue: swapped out verification
• grey: other ```

  Statistical Model Checking

  参考链接：UPPAAL web help](https://www.it.uu.se/research/group/darts/uppaal/help.php?file=Verifier/Verifying.shtml) )

1. Axis meaning
   • y-axis: a probability or its density
   • x-axis denotes either the variable values limited by the statistical query or a step (transition) count in the model run.
2. Probability density distribution
   A histogram created from probability distribution where each bucket is normalized by a bucket width. Useful for comparison of various distributions, potentially with different bucket widths.
3. Probability distribution
   A histogram created from a frequency histogram where each bucket is normalized by a total number of runs. Useful for assessing a probability of a property being satisfied at a particular moment in time interval.
4. Cumulative probability distribution
   A histogram created by adding up all frequency histogram buckets up to the current bucket and normalized by a total number of runs.
5. Confidence Intervals for Probabilities
   The confidence intervals for probabilities are computed using Clopper-Pearson method (also known as “exact”) for binomial distribution for a given level of confidence (1-α). The method is conservative in a sense that it guarantees the minimum coverage of the real probability in (1-α) of cases. In the plots, the estimated confidence is valid only for one bucket at a time (the gathered data is reused to compute each individual bucket).
6. Confidence Intervals for Mean

The confidence intervals for mean estimation are computed using quantiles of Student’s t-distribution for a given level of confidence of 1-α. Note that t-distribution approaches the commonly used Normal (Gaussian) distribution when the number of samples is high.

1. Frequency histogram

   The frequency histogram is created by calculating the number of runs satisfying the property at a particular moment in time interval. Useful for calculating the number of runs.

   相关参考

2. 怎样理解和区分中心极限定理与大数定律？- 知乎

3. 如何通俗地解释「置信区间」和「置信水平」？- 知乎
4. 大数定律具体是个什么概念？- 知乎
5. 如何理解 95% 置信区间？- 知乎