Bluemoon: Documentación

La invocación de la herramienta sigue el estilo del model checker PRISM en el que está inserta. La sintaxis es:

~$ prism-bm <modelfile> <consts>  -rarevent [<type> <strategy>]  \
                              [-rareconf <conf> <prec>[%]]    \
                              [-rareparams "<params>"]

donde:

  • prism-bm es el comando de ejecución de la herramienta,
  • <modelfile> es un path a un archivo de texto plano con el modelo del sistema,
  • <consts> es la lista de definición de valores de constantes de PRISM (ver prism-bm --help const),
  • <type> es 'fhit' o 'freq', y le indica a la herramienta si la propiedad estudiada es transitoria o de estado estacionario respectivamente (ver prism-bm --help rarevent),
  • <strategy> es 'auto', 'adhoc' o 'nosplit', y le indica a la herramienta cual estrategia de simulación usar para la estimación (ver prism-bm --help rarevent),
  • <conf> es un real en el intervalo (0,1) que especifica el coeficiente de confianza deseado (ver prism-bm --help rareconf),
  • <prec> especifica la precisión deseada para el intervalo de confianza, y puede ser cualquier real positivo o un valor porcentual terminado con el caracter % (ver prism-bm --help rareconf),
  • <params> es una lista de argumentos separados por coma que especifica opciones finas para la simulación, donde las opciones son techlog, ifun, effort, split, ci y timeout (ver prism-bm --help rareparams).

A continuación, detallamos las ayudas particulares para cada comando relacionado a Bluemoon:

  • Salida del comando prism-bm --help rarevent:
    Switch: -rarevent [<type> <strategy>]
    
        <type>: fhit*, freq.
    <strategy>: auto*, adhoc, nosplit.
    
    <type> is required for <strategy> specification.
    If neither <type> nor <strategy> are specified, default is "fhit auto".
    
  • Salida del comando prism-bm --help rareconf:
    Switch: -rareconf <conf> <prec>[%]
    
      <conf> gives the desired confidence coefficient ∈ (0.0, 1.0).
      <prec> gives the desired confidence interval length, aka precision.
             This can be any positive number, or alternatively some percentage,
             which will be applied to the average over the first thirty 
             estimations of the rare event probability.
    
    Examples:
     -rareconf 0.95 1E-7
     -rareconf 0.9 5%
    
  • Salida del comando prism-bm --help rareparams:
    Switch: -rareparams "<params>"
    
    <params> is a comma-separated list of parameters for the rare event
    simulation engine, specifying at least one of the following:
      techlog=<name>, where <name> is the name of the file
                       to be used for technical output;
      ifun=<expr>,    where <expr> is an integer typed expression
                       to be used as Ad hoc importance function;
      effort=<val>,   where <val> is a positive integer
                       to be used as each simulation maximum effort;
      split=<val>,    where <val> is an integer greater than 1
                       to be used as split value on threshold level-up;
      ci=<method>,    where <method> specifies the confidence interval
                       construction method to use, which should be
                       one of: "mean", "prop" or "wilson";
      timeout=<val>,  where <val> is a non-negative number of minutes
                       to be used as wall time limit. If 0 == <val>
                       then there is no timeout, and simulation stops
                       once the confidence criteria is met (default)
    
    Examples:
     -rareparams "ifun=q2"
     -rareparams "ifun=x1+x2,split=4"
     -rareparams "split=2,effort=256,ifun=q1+5*q2,ci=wilson"
    

Finalmente, reportamos diversos ejemplos de uso:

Si "tandem.prism" es un archivo de texto plano con el modelo a estudiar, donde las constantes 'c' y 'mu1' están libres, una corrida típica para una propiedad transitoria puede ser:

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent -rareconf .9 40%

o equivalentemente

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent fhit auto \
   -rareconf .9 40%

donde se especificó un nivel de confianza del 90%, una precisión del cuarenta por ciento del valor estimado, y donde se simulará usando división por importancia con la función de importancia automáticamente construida por Bluemoon.

Si quisiéramos hacer lo mismo pero sin utilizar división por importancia, sino simulaciones Monte Carlo estándar, el comando sería:

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent fhit nosplit \
   -rareconf .9 40%

Si en cambio deseamos estudiar una propiedad de estado estacionario, el comando debería ser:

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent freq auto \
   -rareconf .9 40%

Si además queremos usar una función de importancia definida ad hoc pornosotros, digamos q1 + 10 q2, donde q1 y q2 son variables del modelo que asumen valores enteros, el comando debería ser:

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent freq adhoc \
   -rareconf .9 40% -rareparams "ifun=q1+10*q2"

Por último, si deseáramos también indicar que el splitting por threshold debe ser igual a ocho y que los detalles técnicos sean escritos dentro de un archivo con nombre "run5.log", entonces el comando debería ser:

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent freq adhoc \
   -rareconf .9 40% -rareparams "ifun=q1+10*q2,split=8,techlog=run5.log"
Powered by Drupal