Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
T
tlc4b
Manage
Activity
Members
Labels
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Locked files
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Analyze
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
general
stups
tlc4b
Commits
245659f9
Commit
245659f9
authored
11 months ago
by
dgelessus
Browse files
Options
Downloads
Patches
Plain Diff
Inline Log code into main TLC4B class
parent
73e7be5e
No related branches found
No related tags found
No related merge requests found
Changes
2
Show whitespace changes
Inline
Side-by-side
Showing
2 changed files
src/main/java/de/tlc4b/Log.java
+0
-77
0 additions, 77 deletions
src/main/java/de/tlc4b/Log.java
src/main/java/de/tlc4b/TLC4B.java
+63
-1
63 additions, 1 deletion
src/main/java/de/tlc4b/TLC4B.java
with
63 additions
and
78 deletions
src/main/java/de/tlc4b/Log.java
deleted
100644 → 0
+
0
−
77
View file @
73e7be5e
package
de.tlc4b
;
import
static
de
.
tlc4b
.
util
.
StopWatch
.
Watches
.
PARSING_TIME
;
import
java.util.ArrayList
;
import
java.util.List
;
import
java.util.Map
;
import
de.tlc4b.tlc.TLCResults
;
import
de.tlc4b.util.StopWatch
;
import
de.tlc4b.util.StopWatch.Watches
;
public
final
class
Log
{
public
static
final
String
DELIMITER
=
";"
;
private
Log
()
{}
public
static
String
getCSVString
(
TLC4B
tlc4b
,
TLCResults
tlcResults
)
{
List
<
String
>
fieldNames
=
new
ArrayList
<>();
List
<
String
>
fieldValues
=
new
ArrayList
<>();
fieldNames
.
add
(
"Machine File"
);
String
machineFile
=
tlc4b
.
getMainFile
().
getAbsolutePath
();
fieldValues
.
add
(
machineFile
);
fieldNames
.
add
(
"TLC Model Checking Time (s)"
);
double
tlcModelCheckingTime
=
tlcResults
.
getModelCheckingTime
();
fieldValues
.
add
(
String
.
valueOf
(
tlcModelCheckingTime
));
fieldNames
.
add
(
"Parsing Time Of B machine (ms)"
);
long
parseTime
=
StopWatch
.
getRunTime
(
PARSING_TIME
);
fieldValues
.
add
(
String
.
valueOf
(
parseTime
));
fieldNames
.
add
(
"Translation Time (ms)"
);
long
translationTime
=
StopWatch
.
getRunTime
(
Watches
.
TRANSLATION_TIME
);
fieldValues
.
add
(
String
.
valueOf
(
translationTime
));
fieldNames
.
add
(
"Model Checking Time (ms)"
);
long
modelCheckingTime
=
StopWatch
.
getRunTime
(
Watches
.
MODEL_CHECKING_TIME
);
fieldValues
.
add
(
String
.
valueOf
(
modelCheckingTime
));
fieldNames
.
add
(
"TLC Result"
);
fieldValues
.
add
(
tlcResults
.
getResultString
());
fieldNames
.
add
(
"States analysed"
);
fieldValues
.
add
(
Integer
.
toString
(
tlcResults
.
getNumberOfDistinctStates
()));
fieldNames
.
add
(
"Transitions fired"
);
fieldValues
.
add
(
Integer
.
toString
(
tlcResults
.
getNumberOfTransitions
()));
fieldNames
.
add
(
"Violated Definition"
);
String
violatedDefinition
=
tlcResults
.
getViolatedDefinition
();
fieldValues
.
add
(
violatedDefinition
!=
null
?
violatedDefinition
:
""
);
fieldNames
.
add
(
"Violated Assertions"
);
List
<
String
>
violatedAssertions
=
tlcResults
.
getViolatedAssertions
();
fieldValues
.
add
(!
violatedAssertions
.
isEmpty
()
?
String
.
join
(
DELIMITER
,
violatedAssertions
)
:
""
);
fieldNames
.
add
(
"Operation Coverage"
);
Map
<
String
,
Long
>
operationCount
=
tlcResults
.
getOperationCount
();
List
<
String
>
opCountString
=
new
ArrayList
<>();
if
(
operationCount
!=
null
)
{
operationCount
.
forEach
((
operation
,
count
)
->
opCountString
.
add
(
operation
+
DELIMITER
+
count
));
}
fieldValues
.
add
(!
opCountString
.
isEmpty
()
?
String
.
join
(
DELIMITER
,
opCountString
)
:
""
);
fieldNames
.
add
(
"Trace File"
);
fieldValues
.
add
(
tlc4b
.
getTraceFile
()
!=
null
?
tlc4b
.
getTraceFile
().
getAbsolutePath
()
:
""
);
StringBuilder
sb
=
new
StringBuilder
();
for
(
int
i
=
0
;
i
<
fieldNames
.
size
();
i
++)
{
sb
.
append
(
fieldNames
.
get
(
i
)).
append
(
DELIMITER
).
append
(
fieldValues
.
get
(
i
)).
append
(
"\n"
);
}
return
sb
.
toString
();
}
}
This diff is collapsed.
Click to expand it.
src/main/java/de/tlc4b/TLC4B.java
+
63
−
1
View file @
245659f9
...
...
@@ -9,6 +9,8 @@ import java.io.InputStream;
import
java.io.OutputStreamWriter
;
import
java.nio.charset.StandardCharsets
;
import
java.nio.file.Files
;
import
java.util.ArrayList
;
import
java.util.List
;
import
java.util.Map
;
import
java.util.Map.Entry
;
import
java.util.concurrent.ExecutionException
;
...
...
@@ -37,6 +39,7 @@ import static de.tlc4b.util.StopWatch.Watches.*;
import
static
de
.
tlc4b
.
MP
.*;
public
class
TLC4B
{
private
static
final
String
CSV_DELIMITER
=
";"
;
private
String
filename
;
private
File
mainfile
,
traceFile
;
...
...
@@ -419,9 +422,68 @@ public class TLC4B {
}
}
private
String
getLogCsvString
(
TLCResults
tlcResults
)
{
List
<
String
>
fieldNames
=
new
ArrayList
<>();
List
<
String
>
fieldValues
=
new
ArrayList
<>();
fieldNames
.
add
(
"Machine File"
);
String
machineFile
=
this
.
getMainFile
().
getAbsolutePath
();
fieldValues
.
add
(
machineFile
);
fieldNames
.
add
(
"TLC Model Checking Time (s)"
);
double
tlcModelCheckingTime
=
tlcResults
.
getModelCheckingTime
();
fieldValues
.
add
(
String
.
valueOf
(
tlcModelCheckingTime
));
fieldNames
.
add
(
"Parsing Time Of B machine (ms)"
);
long
parseTime
=
StopWatch
.
getRunTime
(
PARSING_TIME
);
fieldValues
.
add
(
String
.
valueOf
(
parseTime
));
fieldNames
.
add
(
"Translation Time (ms)"
);
long
translationTime
=
StopWatch
.
getRunTime
(
TRANSLATION_TIME
);
fieldValues
.
add
(
String
.
valueOf
(
translationTime
));
fieldNames
.
add
(
"Model Checking Time (ms)"
);
long
modelCheckingTime
=
StopWatch
.
getRunTime
(
MODEL_CHECKING_TIME
);
fieldValues
.
add
(
String
.
valueOf
(
modelCheckingTime
));
fieldNames
.
add
(
"TLC Result"
);
fieldValues
.
add
(
tlcResults
.
getResultString
());
fieldNames
.
add
(
"States analysed"
);
fieldValues
.
add
(
Integer
.
toString
(
tlcResults
.
getNumberOfDistinctStates
()));
fieldNames
.
add
(
"Transitions fired"
);
fieldValues
.
add
(
Integer
.
toString
(
tlcResults
.
getNumberOfTransitions
()));
fieldNames
.
add
(
"Violated Definition"
);
String
violatedDefinition
=
tlcResults
.
getViolatedDefinition
();
fieldValues
.
add
(
violatedDefinition
!=
null
?
violatedDefinition
:
""
);
fieldNames
.
add
(
"Violated Assertions"
);
List
<
String
>
violatedAssertions
=
tlcResults
.
getViolatedAssertions
();
fieldValues
.
add
(!
violatedAssertions
.
isEmpty
()
?
String
.
join
(
CSV_DELIMITER
,
violatedAssertions
)
:
""
);
fieldNames
.
add
(
"Operation Coverage"
);
Map
<
String
,
Long
>
operationCount
=
tlcResults
.
getOperationCount
();
List
<
String
>
opCountString
=
new
ArrayList
<>();
if
(
operationCount
!=
null
)
{
operationCount
.
forEach
((
operation
,
count
)
->
opCountString
.
add
(
operation
+
CSV_DELIMITER
+
count
));
}
fieldValues
.
add
(!
opCountString
.
isEmpty
()
?
String
.
join
(
CSV_DELIMITER
,
opCountString
)
:
""
);
fieldNames
.
add
(
"Trace File"
);
fieldValues
.
add
(
this
.
getTraceFile
()
!=
null
?
this
.
getTraceFile
().
getAbsolutePath
()
:
""
);
StringBuilder
sb
=
new
StringBuilder
();
for
(
int
i
=
0
;
i
<
fieldNames
.
size
();
i
++)
{
sb
.
append
(
fieldNames
.
get
(
i
)).
append
(
CSV_DELIMITER
).
append
(
fieldValues
.
get
(
i
)).
append
(
"\n"
);
}
return
sb
.
toString
();
}
private
void
createLogFile
(
TLCResults
results
)
{
if
(
logFileString
!=
null
)
{
String
logCsvString
=
Log
.
getCSV
String
(
this
,
results
);
String
logCsvString
=
getLogCsv
String
(
results
);
File
logFile
=
new
File
(
logFileString
);
try
(
FileWriter
fw
=
new
FileWriter
(
logFile
,
true
))
{
// the true will append the new data
fw
.
write
(
logCsvString
);
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment