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

Update sparse engine adversary generation to include number of transitions in the tra file. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10092 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
5942b9e977
commit
1eb73ab127
2 changed files with 65 additions and 39 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 50
      prism/src/sparse/PS_NondetReachReward.cc
  2. 54
      prism/src/sparse/PS_NondetUntil.cc

50
prism/src/sparse/PS_NondetReachReward.cc
View File

@ -347,25 +347,39 @@ jboolean min // min or max probabilities (true = min, false = max)
// Traverse matrix to extract adversary
if (export_adv_enabled != EXPORT_ADV_NONE) {
h1 = h2 = 0;
for (i = 0; i < n; i++) {
if (!use_counts) { l1 = row_starts[i]; h1 = row_starts[i+1]; }
else { l1 = h1; h1 += row_counts[i]; }
// Have to loop through all choices (to compute offsets)
for (j = l1; j < h1; j++) {
if (!use_counts) { l2 = choice_starts[j]; h2 = choice_starts[j+1]; }
else { l2 = h2; h2 += choice_counts[j]; }
// But only output a choice if it is in the adversary
if (j == adv[i]) {
for (k = l2; k < h2; k++) {
switch (export_adv_enabled) {
case EXPORT_ADV_DTMC:
fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]); break;
case EXPORT_ADV_MDP:
fprintf(fp_adv, "%d 0 %d %g", i, cols[k], non_zeros[k]); break;
// Do two passes: first to compute the number of transitions,
// the second to actually do the export
int num_trans = 0;
for (int pass = 1; pass <= 2; pass++) {
if (pass == 2) {
fprintf(fp_adv, "%d %d\n", n, num_trans);
}
h1 = h2 = 0;
for (i = 0; i < n; i++) {
if (!use_counts) { l1 = row_starts[i]; h1 = row_starts[i+1]; }
else { l1 = h1; h1 += row_counts[i]; }
// Have to loop through all choices (to compute offsets)
for (j = l1; j < h1; j++) {
if (!use_counts) { l2 = choice_starts[j]; h2 = choice_starts[j+1]; }
else { l2 = h2; h2 += choice_counts[j]; }
// But only output a choice if it is in the adversary
if (j == adv[i]) {
switch (pass) {
case 1:
num_trans += (h2-l2);
break;
case 2:
for (k = l2; k < h2; k++) {
switch (export_adv_enabled) {
case EXPORT_ADV_DTMC:
fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]); break;
case EXPORT_ADV_MDP:
fprintf(fp_adv, "%d 0 %d %g", i, cols[k], non_zeros[k]); break;
}
if (ndsm->actions != NULL) fprintf(fp_adv, " %s", ndsm->actions[j]>0?action_names[ndsm->actions[j]-1]:"");
fprintf(fp_adv, "\n");
}
}
if (ndsm->actions != NULL) fprintf(fp_adv, " %s", ndsm->actions[j]>0?action_names[ndsm->actions[j]-1]:"");
fprintf(fp_adv, "\n");
}
}
}

54
prism/src/sparse/PS_NondetUntil.cc
View File

@ -215,9 +215,7 @@ jlong _strat // strategy storage
// open file to store adversary (if required)
if (export_adv_enabled != EXPORT_ADV_NONE) {
fp_adv = fopen(export_adv_filename, "w");
if (fp_adv) {
fprintf(fp_adv, "%d ?\n", n);
} else {
if (!fp_adv) {
PS_PrintWarningToMainLog(env, "Adversary generation cancelled (could not open file \"%s\").", export_adv_filename);
export_adv_enabled = EXPORT_ADV_NONE;
}
@ -304,25 +302,39 @@ jlong _strat // strategy storage
// Traverse matrix to extract adversary
if (export_adv_enabled != EXPORT_ADV_NONE) {
h1 = h2 = 0;
for (i = 0; i < n; i++) {
if (!use_counts) { l1 = row_starts[i]; h1 = row_starts[i+1]; }
else { l1 = h1; h1 += row_counts[i]; }
// Have to loop through all choices (to compute offsets)
for (j = l1; j < h1; j++) {
if (!use_counts) { l2 = choice_starts[j]; h2 = choice_starts[j+1]; }
else { l2 = h2; h2 += choice_counts[j]; }
// But only output a choice if it is in the adversary
if (j == adv[i]) {
for (k = l2; k < h2; k++) {
switch (export_adv_enabled) {
case EXPORT_ADV_DTMC:
fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]); break;
case EXPORT_ADV_MDP:
fprintf(fp_adv, "%d 0 %d %g", i, cols[k], non_zeros[k]); break;
// Do two passes: first to compute the number of transitions,
// the second to actually do the export
int num_trans = 0;
for (int pass = 1; pass <= 2; pass++) {
if (pass == 2) {
fprintf(fp_adv, "%d %d\n", n, num_trans);
}
h1 = h2 = 0;
for (i = 0; i < n; i++) {
if (!use_counts) { l1 = row_starts[i]; h1 = row_starts[i+1]; }
else { l1 = h1; h1 += row_counts[i]; }
// Have to loop through all choices (to compute offsets)
for (j = l1; j < h1; j++) {
if (!use_counts) { l2 = choice_starts[j]; h2 = choice_starts[j+1]; }
else { l2 = h2; h2 += choice_counts[j]; }
// But only output a choice if it is in the adversary
if (j == adv[i]) {
switch (pass) {
case 1:
num_trans += (h2-l2);
break;
case 2:
for (k = l2; k < h2; k++) {
switch (export_adv_enabled) {
case EXPORT_ADV_DTMC:
fprintf(fp_adv, "%d %d %g", i, cols[k], non_zeros[k]); break;
case EXPORT_ADV_MDP:
fprintf(fp_adv, "%d 0 %d %g", i, cols[k], non_zeros[k]); break;
}
if (ndsm->actions != NULL) fprintf(fp_adv, " %s", ndsm->actions[j]>0?action_names[ndsm->actions[j]-1]:"");
fprintf(fp_adv, "\n");
}
}
if (ndsm->actions != NULL) fprintf(fp_adv, " %s", ndsm->actions[j]>0?action_names[ndsm->actions[j]-1]:"");
fprintf(fp_adv, "\n");
}
}
}

Write Preview
Loading…
Cancel
Save