s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

PM: cleanup format strings 

%ld for number of nodes
 %ld for number of iterations / fgw.right (continuous time computations)


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12185 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
e31b05c257
commit
14d652d331
3 changed files with 11 additions and 11 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      prism/src/mtbdd/PM_StochBoundedUntil.cc
  2. 6
      prism/src/mtbdd/PM_StochCumulReward.cc
  3. 8
      prism/src/mtbdd/PM_StochTransient.cc

8
prism/src/mtbdd/PM_StochBoundedUntil.cc
View File

@ -99,7 +99,7 @@ jlong __jlongpointer mu // probs for multiplying
diags = DD_SumAbstract(ddman, trans, cvars, num_rvars); diags = DD_SumAbstract(ddman, trans, cvars, num_rvars);
diags = DD_Apply(ddman, APPLY_TIMES, diags, DD_Constant(ddman, -1)); diags = DD_Apply(ddman, APPLY_TIMES, diags, DD_Constant(ddman, -1));
i = DD_GetNumNodes(ddman, diags); i = DD_GetNumNodes(ddman, diags);
PM_PrintToMainLog(env, "[nodes=%d] [%.1f Kb]\n", i, i*20.0/1024.0);
PM_PrintToMainLog(env, "[nodes=%ld] [%.1f Kb]\n", i, i*20.0/1024.0);
if (combine) { if (combine) {
@ -137,7 +137,7 @@ jlong __jlongpointer mu // probs for multiplying
// PM_PrintToMainLog(env, "Q (final) = %d %d %.0f\n", DD_GetNumNodes(ddman, q), DD_GetNumTerminals(ddman, q), DD_GetNumMinterms(ddman, q, num_rvars+num_cvars)); // PM_PrintToMainLog(env, "Q (final) = %d %d %.0f\n", DD_GetNumNodes(ddman, q), DD_GetNumTerminals(ddman, q), DD_GetNumMinterms(ddman, q, num_rvars+num_cvars));
i = DD_GetNumNodes(ddman, q); i = DD_GetNumNodes(ddman, q);
PM_PrintToMainLog(env, "[nodes=%d] [%.1f Kb]\n", i, i*20.0/1024.0);
PM_PrintToMainLog(env, "[nodes=%ld] [%.1f Kb]\n", i, i*20.0/1024.0);
} }
else { else {
@ -174,7 +174,7 @@ jlong __jlongpointer mu // probs for multiplying
// PM_PrintToMainLog(env, "diags (final) = %d %d %.0f\n", DD_GetNumNodes(ddman, d), DD_GetNumTerminals(ddman, d), DD_GetNumMinterms(ddman, d, num_rvars)); // PM_PrintToMainLog(env, "diags (final) = %d %d %.0f\n", DD_GetNumNodes(ddman, d), DD_GetNumTerminals(ddman, d), DD_GetNumMinterms(ddman, d, num_rvars));
i = DD_GetNumNodes(ddman, r); i = DD_GetNumNodes(ddman, r);
PM_PrintToMainLog(env, "[nodes=%d] [%.1f Kb]\n", i, i*20.0/1024.0);
PM_PrintToMainLog(env, "[nodes=%ld] [%.1f Kb]\n", i, i*20.0/1024.0);
} }
// compute new termination criterion parameter (epsilon/8) // compute new termination criterion parameter (epsilon/8)
@ -294,7 +294,7 @@ jlong __jlongpointer mu // probs for multiplying
// print occasional status update // print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) { if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PM_PrintToMainLog(env, "Iteration %d (of %d): ", iters, fgw.right);
PM_PrintToMainLog(env, "Iteration %ld (of %ld): ", iters, fgw.right);
PM_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000)); PM_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time(); start3 = util_cpu_time();
} }

6
prism/src/mtbdd/PM_StochCumulReward.cc
View File

@ -89,7 +89,7 @@ jdouble time // time bound
diags = DD_SumAbstract(ddman, trans, cvars, num_rvars); diags = DD_SumAbstract(ddman, trans, cvars, num_rvars);
diags = DD_Apply(ddman, APPLY_TIMES, diags, DD_Constant(ddman, -1)); diags = DD_Apply(ddman, APPLY_TIMES, diags, DD_Constant(ddman, -1));
i = DD_GetNumNodes(ddman, diags); i = DD_GetNumNodes(ddman, diags);
PM_PrintToMainLog(env, "[nodes=%d] [%.1f Kb]\n", i, i*20.0/1024.0);
PM_PrintToMainLog(env, "[nodes=%ld] [%.1f Kb]\n", i, i*20.0/1024.0);
PM_PrintToMainLog(env, "Building iteration matrix MTBDD... "); PM_PrintToMainLog(env, "Building iteration matrix MTBDD... ");
@ -112,7 +112,7 @@ jdouble time // time bound
Cudd_Ref(reach); Cudd_Ref(reach);
q = DD_Apply(ddman, APPLY_PLUS, q, DD_Apply(ddman, APPLY_TIMES, DD_Identity(ddman, rvars, cvars, num_rvars), reach)); q = DD_Apply(ddman, APPLY_PLUS, q, DD_Apply(ddman, APPLY_TIMES, DD_Identity(ddman, rvars, cvars, num_rvars), reach));
i = DD_GetNumNodes(ddman, q); i = DD_GetNumNodes(ddman, q);
PM_PrintToMainLog(env, "[nodes=%d] [%.1f Kb]\n", i, i*20.0/1024.0);
PM_PrintToMainLog(env, "[nodes=%ld] [%.1f Kb]\n", i, i*20.0/1024.0);
// combine state/transition rewards into a single vector - this is the initial solution vector // combine state/transition rewards into a single vector - this is the initial solution vector
Cudd_Ref(trans); Cudd_Ref(trans);
@ -212,7 +212,7 @@ jdouble time // time bound
// print occasional status update // print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) { if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PM_PrintToMainLog(env, "Iteration %d (of %d): ", iters, fgw.right);
PM_PrintToMainLog(env, "Iteration %ld (of %ld): ", iters, fgw.right);
PM_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000)); PM_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time(); start3 = util_cpu_time();
} }

8
prism/src/mtbdd/PM_StochTransient.cc
View File

@ -91,7 +91,7 @@ jdouble time // time
diags = DD_SumAbstract(ddman, trans, cvars, num_rvars); diags = DD_SumAbstract(ddman, trans, cvars, num_rvars);
diags = DD_Apply(ddman, APPLY_TIMES, diags, DD_Constant(ddman, -1)); diags = DD_Apply(ddman, APPLY_TIMES, diags, DD_Constant(ddman, -1));
i = DD_GetNumNodes(ddman, diags); i = DD_GetNumNodes(ddman, diags);
PM_PrintToMainLog(env, "[nodes=%d] [%.1f Kb]\n", i, i*20.0/1024.0);
PM_PrintToMainLog(env, "[nodes=%ld] [%.1f Kb]\n", i, i*20.0/1024.0);
if (combine) { if (combine) {
@ -121,7 +121,7 @@ jdouble time // time
// PM_PrintToMainLog(env, "Q (final) = %d %d %.0f\n", DD_GetNumNodes(ddman, q), DD_GetNumTerminals(ddman, q), DD_GetNumMinterms(ddman, q, num_rvars+num_cvars)); // PM_PrintToMainLog(env, "Q (final) = %d %d %.0f\n", DD_GetNumNodes(ddman, q), DD_GetNumTerminals(ddman, q), DD_GetNumMinterms(ddman, q, num_rvars+num_cvars));
i = DD_GetNumNodes(ddman, q); i = DD_GetNumNodes(ddman, q);
PM_PrintToMainLog(env, "[nodes=%d] [%.1f Kb]\n", i, i*20.0/1024.0);
PM_PrintToMainLog(env, "[nodes=%ld] [%.1f Kb]\n", i, i*20.0/1024.0);
} }
else { else {
@ -155,7 +155,7 @@ jdouble time // time
diags = DD_PermuteVariables(ddman, diags, rvars, cvars, num_rvars); diags = DD_PermuteVariables(ddman, diags, rvars, cvars, num_rvars);
i = DD_GetNumNodes(ddman, r); i = DD_GetNumNodes(ddman, r);
PM_PrintToMainLog(env, "[nodes=%d] [%.1f Kb]\n", i, i*20.0/1024.0);
PM_PrintToMainLog(env, "[nodes=%ld] [%.1f Kb]\n", i, i*20.0/1024.0);
} }
// compute new termination criterion parameter (epsilon/8) // compute new termination criterion parameter (epsilon/8)
@ -270,7 +270,7 @@ jdouble time // time
// print occasional status update // print occasional status update
if ((util_cpu_time() - start3) > UPDATE_DELAY) { if ((util_cpu_time() - start3) > UPDATE_DELAY) {
PM_PrintToMainLog(env, "Iteration %d (of %d): ", iters, fgw.right);
PM_PrintToMainLog(env, "Iteration %ld (of %ld): ", iters, fgw.right);
PM_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000)); PM_PrintToMainLog(env, "%.2f sec so far\n", ((double)(util_cpu_time() - start2)/1000));
start3 = util_cpu_time(); start3 = util_cpu_time();
} }

Write Preview
Loading…
Cancel
Save