[specs] Using 10 schedules for random exploration can be insufficient for correctness checking/fuzzing

As shown in the referred script
https://github.com/deepseek-ai/3FS/blob/c450ee0cf7b422c53337d585a314c7a6b66405ff/specs/RunTests.ps1#L6

Testing with PChecker only takes 10 schedules. This can be insufficient. By default, PChecker (the fuzzer of P model) uses random exploration. What it does is basically configuring the model instances with non-deterministic inputs and exploring different orders of `event` interleaving. Therefore, 10 schedules may not expose enough behaviors of the P model hence *low confidence for correctness*. **We would suggest using more schedules, e.g., 10k.**

We assume the reason using 10 instead of more is that it usually takes too long for PChecker to finish with the checking models, especially DataStorage. This usually is due to instantiating multiple `Timer`s in the P model. Timers can drastically slow down PChecker since the way it issues `eTimeOut` is through a non-deterministic check as shown below
https://github.com/deepseek-ai/3FS/blob/c450ee0cf7b422c53337d585a314c7a6b66405ff/specs/Timer/PSrc/Timer.p#L15-L34

If the non-deterministic check failed, it cycles back to the same state. This creates a lot of event redundancies (especially when there are multiple timers) during random exploration by the `eDelayTimeOut` events. This can easily exhaust the maximum number of steps. A potential workaround is:
instead of assigning each component a timer to inform about the timeout, use a "ghost" view server to have a central control of timeout. An example is here: https://github.com/AD1024/P-Tutorial-Raft/blob/44d2e349a804109d1c1dcc2658dcf89d441d8880/PSrc/View.p#L128-L184
The idea is that when an `eTimeOut` occurs, the view server randomly chooses some components and inform them about the timeout event. This way, PChecker will not be overwhelmed by the `eDelayTimeOut` events.

Hope this might help with the P modeling.