001package daikon.inv; 002 003import java.util.ArrayList; 004import java.util.List; 005import java.util.StringTokenizer; 006import org.checkerframework.checker.nullness.qual.Nullable; 007import org.checkerframework.dataflow.qual.Pure; 008 009/** 010 * Container class for holding all info needed to describe an Invariant. If any field is null, that 011 * field is a wildcard, so one instance of InvariantInfo may describe multiple Invariants in that 012 * way. 013 */ 014public class InvariantInfo { 015 016 private String ppt; 017 018 // vars is maintained as "var1,var2,.." sorted in ascending lexicographical order 019 /** If null, treated as a wildcard. */ 020 private final @Nullable String vars; 021 022 /** If null, treated as a wildcard. */ 023 private @Nullable String className; 024 025 // private InvariantInfo() { 026 // // Make the default constructor private, this should never be called 027 // } 028 029 /* // It's ok if vars isn't given in sorted order, we'll sort it here */ 030 public InvariantInfo(String ppt, @Nullable String vars, @Nullable String className) { 031 this.ppt = ppt; 032 this.className = className; 033 /* if (vars != null) { 034 // Sort the vars into ascending order 035 StringTokenizer st = new StringTokenizer(vars, ","); 036 ArrayList temp = new ArrayList(); 037 while (st.hasMoreTokens()) { 038 temp.add(st.nextToken()); 039 } 040 Collections.sort(temp); 041 String vars_result = ""; 042 for (int i = 0; i < temp.size(); i++) { 043 vars_result += temp.get(i) + ","; 044 } 045 this.vars = vars_result; 046 }*/ 047 this.vars = vars; 048 } 049 050 public String ppt() { 051 return this.ppt; 052 } 053 054 @Pure 055 public @Nullable String className() { 056 return this.className; 057 } 058 059 public @Nullable String vars() { 060 return this.vars; 061 } 062 063 /** 064 * Returns a list of Strings of all permutations of the vars, or null if vars == null. 065 * 066 * <p>e.g., if vars is "var1,var2,var3", this method will return ["var1,var2,var3", 067 * "var1,var3,var2", "var2,var1,var3"... etc.] 068 * 069 * @return a list of Strings of all permutations of the vars, or null if vars == null 070 */ 071 public @Nullable List<String> var_permutations() { 072 if (vars == null) { 073 return null; 074 } 075 076 // We know there can be at most 3 vars so it's not worth writing 077 // a complicated routine that generates all permutations 078 StringTokenizer st = new StringTokenizer(vars, ","); 079 assert st.countTokens() <= 3; 080 ArrayList<String> result = new ArrayList<>(3); 081 if (st.countTokens() == 1) { 082 result.add(vars); 083 return result; 084 } else if (st.countTokens() == 2) { 085 result.add(vars); 086 String var1 = st.nextToken(); 087 String var2 = st.nextToken(); 088 result.add(var2 + "," + var1); 089 return result; 090 } else { 091 // st.countTokens() == 3 092 String var1 = st.nextToken(); 093 String var2 = st.nextToken(); 094 String var3 = st.nextToken(); 095 result.add(var1 + "," + var2 + "," + var3); 096 result.add(var1 + "," + var3 + "," + var2); 097 result.add(var2 + "," + var1 + "," + var3); 098 result.add(var2 + "," + var3 + "," + var1); 099 result.add(var3 + "," + var1 + "," + var2); 100 result.add(var3 + "," + var2 + "," + var1); 101 return result; 102 } 103 } 104}