TCS / Software / lbtt / FormulaOptions Block Generator

FormulaOptions Block Generator for lbtt

[Help]


= 0); } /*************************************************************************** * Display an error message. */ function showError($msg) { echo "

$msg

\n"; } /*************************************************************************** * Operator map. The key of each element is the "human-readable" name of * the operator, and the value is an array with elements * 0 -- Symbol of the operator. * 1 -- Name of the operator in lbtt's configuration file. * 'arity' -- Arity of the operator. */ $ops = array('Negation' => array(0 => '!', 1 => 'Not', 'arity' => 1), 'Next Time' => array(0 => 'X', 1 => 'Next', 'arity' => 1), 'Finally' => array(0 => '<>', 1 => 'Finally', 'arity' => 1), 'Globally' => array(0 => '[]', 1 => 'Globally', 'arity' => 1), 'Conjunction' => array(0 => '/\\', 1 => 'And', 'arity' => 2), 'Disjunction' => array(0 => '\\/', 1 => 'Or', 'arity' => 2), 'Implication' => array(0 => '->', 1 => 'Implication', 'arity' => 2), 'Equivalence' => array(0 => '<->', 1 => 'Equivalence', 'arity' => 2), 'Exclusive or' => array(0 => 'xor', 1 => 'Xor', 'arity' => 2), 'Until' => array(0 => 'U', 1 => 'Until', 'arity' => 2), 'Release' => array(0 => 'V', 1 => 'Release', 'arity' => 2), 'Weak until' => array(0 => 'W', 1 => 'WeakUntil', 'arity' => 2), 'Strong release' => array(0 => 'M', 1 => 'StrongRelease', 'arity' => 2), 'Before' => array(0 => 'B', 1 => 'Before', 'arity' => 2)); /*************************************************************************** * Directory that stores all local files used by the script. */ $base_dir = '/var/www/Software/lbtt/priorities'; ini_set('display_errors', 0); ini_set('log_errors', 1); ini_set('error_log', "${base_dir}/error_log"); // If the request for the page was not a POST request, initialize the // form parameters to default values; otherwise process the form data. if (strcmp($HTTP_SERVER_VARS['REQUEST_METHOD'], 'POST')) { // Initialize default values for all formula parameters. $formula_size = 5; $create_full_block = true; $num_propositions = 5; $proposition_priority = 90; $true_priority = 5; $false_priority = 5; $generation_interval = 1; $seed = 0; $mode = 'Absolute'; while (list($op) = each($ops)) { $priorities[$op] = '0'; } } else { $values_ok = true; // Will be set to false if there is a problem with the // formula parameters. // Read the formula parameters. $formula_size = $HTTP_POST_VARS['size']; $create_full_block = (strcmp($HTTP_POST_VARS['createfullblock'], 'on') == 0); $num_propositions = $HTTP_POST_VARS['numprops']; $proposition_priority = $HTTP_POST_VARS['priprops']; $true_priority = $HTTP_POST_VARS['pritrue']; $false_priority = $HTTP_POST_VARS['prifalse']; $generation_interval = $HTTP_POST_VARS['geninterval']; $seed = $HTTP_POST_VARS['seed']; $mode = $HTTP_POST_VARS['mode']; // Verify that the formula size is positive. if (!isNonnegInt($formula_size) || intval($formula_size) == 0) { $values_ok = false; } // If a full FormulaOptions block was requested, validate the optional // formula parameters. if ($create_full_block) { if (!isNonnegInt($num_propositions) || !isNonnegInt($proposition_priority) || !isNonnegInt($true_priority) || !isNonnegInt($false_priority)) { $values_ok = false; } } $unary_ops_present = false; // Will be set to true if at least one // unary operator has a nonzero priority. $zero_priorities_present = false; // Will be set to true if one of the // operators has a zero priority. // Verify that each priority is a nonnegative integer. Determine also the // correct values of $unary_ops_present and $zero_priorities_present. while (list($op, $op_info) = each($ops)) { $val = $HTTP_POST_VARS[$op_info[1]]; $priorities[$op] = $val; if (!isNonnegInt($val)) { $values_ok = false; } else if (intval($val) > 0 && $op_info['arity'] == 1) { $unary_ops_present = true; } else if (intval($val) == 0) { $zero_priorities_present = true; } } if (!$values_ok) { echo "

Errors in parameters.

\n"; } else { if (!$unary_ops_present && intval($formula_size) > 1) { showError('Error: At least one unary operator must have a nonzero distribution.'); } else if ($create_full_block && (intval($num_propositions) == 0 || intval($proposition_priority) == 0) && intval($true_priority) == 0 && intval($false_priority) == 0) { showError('Error: There must be at least one atomic formula with a nonzero priority.'); } else { if (!strcmp($HTTP_POST_VARS['mode'], 'Relative')) { $num_unary_ops = 0; $num_binary_ops = 0; $values_found = false; // Will be set to true if the result is found // in the database. $query_msg = '[' . date('j M Y G:i:s') . '] ' . $HTTP_SERVER_VARS['REMOTE_ADDR'] . ': '; // Calculate the sums of the relative priorities of all unary // operators and all binary operators. Construct also a message with // information about the query (to be recorded into the log file). reset($ops); while (list($op, $info) = each($ops)) { if ($info['arity'] == 1) { $num_unary_ops += intval($priorities[$op]); } else { $num_binary_ops += intval($priorities[$op]); } if (intval($priorities[$op]) > 0) { $query_msg .= $info[0] . ' (' . $priorities[$op] . '); '; } } // Normalize the sums. if ($num_unary_ops > 0 && $num_binary_ops > 0) { $d = gcd($num_unary_ops, $num_binary_ops); $num_unary_ops = intval($num_unary_ops / $d); $num_binary_ops = intval($num_binary_ops / $d); } // Read the corresponding absolute priorities from a file and // calculate the final result. if (($file = fopen("{$base_dir}/{$num_unary_ops}.{$num_binary_ops}", 'rb')) && flock($file, LOCK_SH)) { while (!feof($file)) { // Each line of the file is of the form // [Formula size] [# Unary pps] [# Binary ops] // [Priority for unary ops] [Priority for binary ops] // [Abs(Expected#(unary ops)-Expected#(binary ops))] $data = fscanf($file, "%d %d %d %d %d %f\n"); if ($data[0] == $formula_size) { reset($priorities); while (list($op, $pri) = each($priorities)) { $disp_priorities[$op] = $priorities[$op] * $data[2 + $ops[$op]['arity']]; } $values_found = true; break; } } flock($file, LOCK_UN); fclose($file); // Record the query to a log file. if (($file = fopen("{$base_dir}/query_log", 'ab')) && flock($file, LOCK_EX)) { $query_msg .= ($values_found ? 'ok' : 'failed'); fputs($file, "$query_msg\n"); flock($file, LOCK_UN); fclose($file); } } } else { // Construct the result directly from the parameters specified in // the form. while (list($op, $pri) = each($priorities)) { $disp_priorities[$op] = $priorities[$op]; } $values_found = true; } // If the result could not be constructed, display an error message; // otherwise display the result. if (!$values_found) { showError('The parameters for the specified combination of formula size and relative distribution do not exist in the database.'); } else { echo "

";
          if ($create_full_block)
          {
            echo "FormulaOptions\n{\n";
          }
          echo "  Size = $formula_size\n\n",
               "  GenerateMode = Normal\n",
               "  OutputMode = Normal\n",
               "  AbbreviatedOperators = Yes\n";

          if ($create_full_block)
          {
            echo "  ChangeInterval = $generation_interval\n",
                 "  RandomSeed = $seed\n\n",
                 "  Propositions = $num_propositions\n",
                 "  PropositionPriority = $proposition_priority\n",
                 "  TruePriority = $true_priority\n",
                 "  FalsePriority = $false_priority\n";
          }

          echo "\n";

          // Output a definition for the default operator priority only if some
          // operator has a zero priority.

          if ($zero_priorities_present)
          {
            echo "  DefaultOperatorPriority = 0\n";
          }

          reset($ops);
          while (list($op, $info) = each($ops))
          {
            if ($priorities[$op] > 0)
            {    
              echo "  {$info[1]}Priority = $disp_priorities[$op]\n";
            }
          }
          if ($create_full_block)
          {
            echo "}\n";
          }
          echo "

\n\n
\n\n"; } } } } echo "\n
\n"; ?> \n"; echo " \n"; echo " \n"; if (!$sanity_check) { echo " \n"; } echo "\n"; } function formatPriorityField($op) { global $ops, $priorities; $info = $ops[$op]; echo " \n", " \n", " \n"; } /**************************************************************************** * Error messages. */ $expect_positive_integer = 'Positive integer expected.'; $expect_nonneg_integer = 'Nonnegative integer expected.'; // Construct the form for setting formula parameters. formatNonPriorityRow('Formula size', 'size', $formula_size, isNonnegInt($formula_size) && intval($formula_size) > 0, $expect_positive_integer); echo "\n \n \n\n"; formatNonPriorityRow('Number of atomic propositions', 'numprops', $num_propositions, !$create_full_block || isNonnegInt($num_propositions), $expect_nonneg_integer); formatNonPriorityRow('Priority for propositions', 'priprops', $proposition_priority, !$create_full_block || isNonnegInt($proposition_priority), $expect_nonneg_integer); formatNonPriorityRow('Priority for true', 'pritrue', $true_priority, !$create_full_block || isNonnegInt($true_priority), $expect_nonneg_integer); formatNonPriorityRow('Priority for false', 'prifalse', $false_priority, !$create_full_block || isNonnegInt($false_priority), $expect_nonneg_integer); formatNonPriorityRow('Formula generation interval', 'geninterval', $generation_interval, !$create_full_block || isNonnegInt($generation_interval), $expect_nonneg_integer); formatNonPriorityRow('Random seed', 'seed', $seed, !$create_full_block || isNonnegInt($seed), $expect_nonneg_integer); ?>
Formula parameters
{$label}  \n"; echo " \n"; echo " \n"; echo "   $msg\n"; echo "
"; if (!isNonnegInt($priorities[$op])) { echo ""; } echo "{$op}  "; if (!isNonnegInt($priorities[$op])) { echo ""; } echo "($info[0])  
\n Create a full FormulaOptions block\n", " \n \n

Select interpretation of priorities: \n

\n"; ?> \n"; if (current($unary_ops)) { formatPriorityField(current($unary_ops)); } else { echo " \n \n \n"; } echo " \n"; if (current($binary_ops)) { formatPriorityField(current($binary_ops)); } echo "\n"; next($unary_ops); next($binary_ops); } ?>
Operator priorities
Unary operators Binary operators
  


Fill in the above form with desired formula parameters and then hit the `Generate' button to generate a corresponding fragment of a FormulaOptions block, which can be included into an lbtt configuration file.

Uncheck the `Create a full FormulaOptions block' checkbox to generate only the settings that define the operator priorities. (In this case, the parameters listed under the checkbox can be left unspecified.)

There are two ways to interpret the specified operator priorities: